-- |
-- Module           : Lang.Crucible.LLVM.Errors.UndefinedBehavior
-- Description      : All about undefined behavior
-- Copyright        : (c) Galois, Inc 2018
-- License          : BSD3
-- Maintainer       : Langston Barrett <lbarrett@galois.com>
-- Stability        : provisional
--
-- This module is intended to be imported qualified.
--
-- This module serves as an ad-hoc reference for the sort of undefined behaviors
-- that the Crucible LLVM memory model is aware of. The information contained
-- here is used in
--  * providing helpful error messages
--  * configuring which safety checks to perform
--
-- Disabling checks for undefined behavior does not change the behavior of any
-- memory operations. If it is used to enable the simulation of undefined
-- behavior, the result is that any guarantees that Crucible provides about the
-- code essentially have an additional hypothesis: that the LLVM
-- compiler/hardware platform behave identically to Crucible's simulator when
-- encountering such behavior.
--------------------------------------------------------------------------

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StrictData #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}

module Lang.Crucible.LLVM.Errors.UndefinedBehavior
  (
  -- ** Undefined Behavior
    PtrComparisonOperator(..)
  , UndefinedBehavior(..)
  , cite
  , details
  , explain
  , ppDetails
  , ppCitation
  , pp

  , concUB
  ) where

import           Prelude

import           GHC.Generics (Generic)
import           Data.Data (Data)
import           Data.Kind (Type)
import           Data.Maybe (isJust)
import           Data.Typeable (Typeable)
import           Prettyprinter

import           Data.Parameterized.Classes (toOrdering, fromOrdering)
import           Data.Parameterized.ClassesC (TestEqualityC(..), OrdC(..))
import qualified Data.Parameterized.TH.GADT as U
import           Data.Parameterized.TraversableF (FunctorF(..), FoldableF(..), TraversableF(..))
import qualified Data.Parameterized.TraversableF as TF

import qualified What4.Interface as W4I
import           What4.Expr (GroundValue)

import           Lang.Crucible.Types
import           Lang.Crucible.Simulator.RegValue (RegValue'(..))
import           Lang.Crucible.LLVM.DataLayout (Alignment, fromAlignment)
import           Lang.Crucible.LLVM.Errors.Standards
import qualified Lang.Crucible.LLVM.Errors.Poison as Poison
import           Lang.Crucible.LLVM.MemModel.Pointer (ppPtr, concBV, concPtr')
import           Lang.Crucible.LLVM.MemModel.Type (StorageType)
import           Lang.Crucible.LLVM.Types (LLVMPointerType)

-- -----------------------------------------------------------------------
-- ** UndefinedBehavior

-- | The various comparison operators you can use on pointers
data PtrComparisonOperator =
    Eq
  | Leq
  deriving (Typeable PtrComparisonOperator
Typeable PtrComparisonOperator =>
(forall (c :: Type -> Type).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> PtrComparisonOperator
 -> c PtrComparisonOperator)
-> (forall (c :: Type -> Type).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c PtrComparisonOperator)
-> (PtrComparisonOperator -> Constr)
-> (PtrComparisonOperator -> DataType)
-> (forall (t :: Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c PtrComparisonOperator))
-> (forall (t :: Type -> Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c PtrComparisonOperator))
-> ((forall b. Data b => b -> b)
    -> PtrComparisonOperator -> PtrComparisonOperator)
-> (forall r r'.
    (r -> r' -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> PtrComparisonOperator
    -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> PtrComparisonOperator
    -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> PtrComparisonOperator -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> PtrComparisonOperator -> u)
-> (forall (m :: Type -> Type).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> PtrComparisonOperator -> m PtrComparisonOperator)
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> PtrComparisonOperator -> m PtrComparisonOperator)
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> PtrComparisonOperator -> m PtrComparisonOperator)
-> Data PtrComparisonOperator
PtrComparisonOperator -> Constr
PtrComparisonOperator -> DataType
(forall b. Data b => b -> b)
-> PtrComparisonOperator -> PtrComparisonOperator
forall a.
Typeable a =>
(forall (c :: Type -> Type).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: Type -> Type).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: Type -> Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: Type -> Type).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> PtrComparisonOperator -> u
forall u.
(forall d. Data d => d -> u) -> PtrComparisonOperator -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PtrComparisonOperator -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PtrComparisonOperator -> r
forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d)
-> PtrComparisonOperator -> m PtrComparisonOperator
forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> PtrComparisonOperator -> m PtrComparisonOperator
forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PtrComparisonOperator
forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> PtrComparisonOperator
-> c PtrComparisonOperator
forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PtrComparisonOperator)
forall (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PtrComparisonOperator)
$cgfoldl :: forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> PtrComparisonOperator
-> c PtrComparisonOperator
gfoldl :: forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> PtrComparisonOperator
-> c PtrComparisonOperator
$cgunfold :: forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PtrComparisonOperator
gunfold :: forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PtrComparisonOperator
$ctoConstr :: PtrComparisonOperator -> Constr
toConstr :: PtrComparisonOperator -> Constr
$cdataTypeOf :: PtrComparisonOperator -> DataType
dataTypeOf :: PtrComparisonOperator -> DataType
$cdataCast1 :: forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PtrComparisonOperator)
dataCast1 :: forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PtrComparisonOperator)
$cdataCast2 :: forall (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PtrComparisonOperator)
dataCast2 :: forall (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PtrComparisonOperator)
$cgmapT :: (forall b. Data b => b -> b)
-> PtrComparisonOperator -> PtrComparisonOperator
gmapT :: (forall b. Data b => b -> b)
-> PtrComparisonOperator -> PtrComparisonOperator
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PtrComparisonOperator -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PtrComparisonOperator -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PtrComparisonOperator -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PtrComparisonOperator -> r
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> PtrComparisonOperator -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> PtrComparisonOperator -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> PtrComparisonOperator -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> PtrComparisonOperator -> u
$cgmapM :: forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d)
-> PtrComparisonOperator -> m PtrComparisonOperator
gmapM :: forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d)
-> PtrComparisonOperator -> m PtrComparisonOperator
$cgmapMp :: forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> PtrComparisonOperator -> m PtrComparisonOperator
gmapMp :: forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> PtrComparisonOperator -> m PtrComparisonOperator
$cgmapMo :: forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> PtrComparisonOperator -> m PtrComparisonOperator
gmapMo :: forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> PtrComparisonOperator -> m PtrComparisonOperator
Data, PtrComparisonOperator -> PtrComparisonOperator -> Bool
(PtrComparisonOperator -> PtrComparisonOperator -> Bool)
-> (PtrComparisonOperator -> PtrComparisonOperator -> Bool)
-> Eq PtrComparisonOperator
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PtrComparisonOperator -> PtrComparisonOperator -> Bool
== :: PtrComparisonOperator -> PtrComparisonOperator -> Bool
$c/= :: PtrComparisonOperator -> PtrComparisonOperator -> Bool
/= :: PtrComparisonOperator -> PtrComparisonOperator -> Bool
Eq, (forall x. PtrComparisonOperator -> Rep PtrComparisonOperator x)
-> (forall x. Rep PtrComparisonOperator x -> PtrComparisonOperator)
-> Generic PtrComparisonOperator
forall x. Rep PtrComparisonOperator x -> PtrComparisonOperator
forall x. PtrComparisonOperator -> Rep PtrComparisonOperator x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. PtrComparisonOperator -> Rep PtrComparisonOperator x
from :: forall x. PtrComparisonOperator -> Rep PtrComparisonOperator x
$cto :: forall x. Rep PtrComparisonOperator x -> PtrComparisonOperator
to :: forall x. Rep PtrComparisonOperator x -> PtrComparisonOperator
Generic, Int -> PtrComparisonOperator
PtrComparisonOperator -> Int
PtrComparisonOperator -> [PtrComparisonOperator]
PtrComparisonOperator -> PtrComparisonOperator
PtrComparisonOperator
-> PtrComparisonOperator -> [PtrComparisonOperator]
PtrComparisonOperator
-> PtrComparisonOperator
-> PtrComparisonOperator
-> [PtrComparisonOperator]
(PtrComparisonOperator -> PtrComparisonOperator)
-> (PtrComparisonOperator -> PtrComparisonOperator)
-> (Int -> PtrComparisonOperator)
-> (PtrComparisonOperator -> Int)
-> (PtrComparisonOperator -> [PtrComparisonOperator])
-> (PtrComparisonOperator
    -> PtrComparisonOperator -> [PtrComparisonOperator])
-> (PtrComparisonOperator
    -> PtrComparisonOperator -> [PtrComparisonOperator])
-> (PtrComparisonOperator
    -> PtrComparisonOperator
    -> PtrComparisonOperator
    -> [PtrComparisonOperator])
-> Enum PtrComparisonOperator
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: PtrComparisonOperator -> PtrComparisonOperator
succ :: PtrComparisonOperator -> PtrComparisonOperator
$cpred :: PtrComparisonOperator -> PtrComparisonOperator
pred :: PtrComparisonOperator -> PtrComparisonOperator
$ctoEnum :: Int -> PtrComparisonOperator
toEnum :: Int -> PtrComparisonOperator
$cfromEnum :: PtrComparisonOperator -> Int
fromEnum :: PtrComparisonOperator -> Int
$cenumFrom :: PtrComparisonOperator -> [PtrComparisonOperator]
enumFrom :: PtrComparisonOperator -> [PtrComparisonOperator]
$cenumFromThen :: PtrComparisonOperator
-> PtrComparisonOperator -> [PtrComparisonOperator]
enumFromThen :: PtrComparisonOperator
-> PtrComparisonOperator -> [PtrComparisonOperator]
$cenumFromTo :: PtrComparisonOperator
-> PtrComparisonOperator -> [PtrComparisonOperator]
enumFromTo :: PtrComparisonOperator
-> PtrComparisonOperator -> [PtrComparisonOperator]
$cenumFromThenTo :: PtrComparisonOperator
-> PtrComparisonOperator
-> PtrComparisonOperator
-> [PtrComparisonOperator]
enumFromThenTo :: PtrComparisonOperator
-> PtrComparisonOperator
-> PtrComparisonOperator
-> [PtrComparisonOperator]
Enum, Eq PtrComparisonOperator
Eq PtrComparisonOperator =>
(PtrComparisonOperator -> PtrComparisonOperator -> Ordering)
-> (PtrComparisonOperator -> PtrComparisonOperator -> Bool)
-> (PtrComparisonOperator -> PtrComparisonOperator -> Bool)
-> (PtrComparisonOperator -> PtrComparisonOperator -> Bool)
-> (PtrComparisonOperator -> PtrComparisonOperator -> Bool)
-> (PtrComparisonOperator
    -> PtrComparisonOperator -> PtrComparisonOperator)
-> (PtrComparisonOperator
    -> PtrComparisonOperator -> PtrComparisonOperator)
-> Ord PtrComparisonOperator
PtrComparisonOperator -> PtrComparisonOperator -> Bool
PtrComparisonOperator -> PtrComparisonOperator -> Ordering
PtrComparisonOperator
-> PtrComparisonOperator -> PtrComparisonOperator
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: PtrComparisonOperator -> PtrComparisonOperator -> Ordering
compare :: PtrComparisonOperator -> PtrComparisonOperator -> Ordering
$c< :: PtrComparisonOperator -> PtrComparisonOperator -> Bool
< :: PtrComparisonOperator -> PtrComparisonOperator -> Bool
$c<= :: PtrComparisonOperator -> PtrComparisonOperator -> Bool
<= :: PtrComparisonOperator -> PtrComparisonOperator -> Bool
$c> :: PtrComparisonOperator -> PtrComparisonOperator -> Bool
> :: PtrComparisonOperator -> PtrComparisonOperator -> Bool
$c>= :: PtrComparisonOperator -> PtrComparisonOperator -> Bool
>= :: PtrComparisonOperator -> PtrComparisonOperator -> Bool
$cmax :: PtrComparisonOperator
-> PtrComparisonOperator -> PtrComparisonOperator
max :: PtrComparisonOperator
-> PtrComparisonOperator -> PtrComparisonOperator
$cmin :: PtrComparisonOperator
-> PtrComparisonOperator -> PtrComparisonOperator
min :: PtrComparisonOperator
-> PtrComparisonOperator -> PtrComparisonOperator
Ord, ReadPrec [PtrComparisonOperator]
ReadPrec PtrComparisonOperator
Int -> ReadS PtrComparisonOperator
ReadS [PtrComparisonOperator]
(Int -> ReadS PtrComparisonOperator)
-> ReadS [PtrComparisonOperator]
-> ReadPrec PtrComparisonOperator
-> ReadPrec [PtrComparisonOperator]
-> Read PtrComparisonOperator
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS PtrComparisonOperator
readsPrec :: Int -> ReadS PtrComparisonOperator
$creadList :: ReadS [PtrComparisonOperator]
readList :: ReadS [PtrComparisonOperator]
$creadPrec :: ReadPrec PtrComparisonOperator
readPrec :: ReadPrec PtrComparisonOperator
$creadListPrec :: ReadPrec [PtrComparisonOperator]
readListPrec :: ReadPrec [PtrComparisonOperator]
Read, Int -> PtrComparisonOperator -> ShowS
[PtrComparisonOperator] -> ShowS
PtrComparisonOperator -> [Char]
(Int -> PtrComparisonOperator -> ShowS)
-> (PtrComparisonOperator -> [Char])
-> ([PtrComparisonOperator] -> ShowS)
-> Show PtrComparisonOperator
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PtrComparisonOperator -> ShowS
showsPrec :: Int -> PtrComparisonOperator -> ShowS
$cshow :: PtrComparisonOperator -> [Char]
show :: PtrComparisonOperator -> [Char]
$cshowList :: [PtrComparisonOperator] -> ShowS
showList :: [PtrComparisonOperator] -> ShowS
Show)

ppPtrComparison :: PtrComparisonOperator -> Doc ann
ppPtrComparison :: forall ann. PtrComparisonOperator -> Doc ann
ppPtrComparison PtrComparisonOperator
Eq  = Doc ann
"Equality comparison (==)"
ppPtrComparison PtrComparisonOperator
Leq = Doc ann
"Ordering comparison (<=)"

-- | This type is parameterized on a higher-kinded term constructor so that it
-- can be instantiated for expressions at translation time (i.e. the 'Expr' in
-- 'LLVMGenerator'), or for expressions at runtime ('SymExpr').
--
-- See 'cite' and 'explain' for what each constructor means at the C/LLVM level.
--
-- The commented-out constructors correspond to behaviors that don't have
-- explicit checks yet (but probably should!).
data UndefinedBehavior (e :: CrucibleType -> Type) where

  -- -------------------------------- Memory management

  FreeBadOffset ::
    (1 <= w) =>
    e (LLVMPointerType w) ->
    UndefinedBehavior e

  FreeUnallocated ::
    (1 <= w) =>
    e (LLVMPointerType w) ->
    UndefinedBehavior e

  DoubleFree ::
    (1 <= w) =>
    e (LLVMPointerType w) ->
    UndefinedBehavior e

  -- | Arguments: Destination pointer, fill byte, length
  MemsetInvalidRegion ::
    (1 <= w, 1 <= v) =>
    e (LLVMPointerType w) ->
    e (BVType 8) ->
    e (BVType v) ->
    UndefinedBehavior e

  -- | Arguments: Read destination, alignment
  ReadBadAlignment ::
    (1 <= w) =>
    e (LLVMPointerType w) ->
    Alignment ->
    UndefinedBehavior e

  -- | Arguments: Write destination, alignment
  WriteBadAlignment ::
    (1 <= w) =>
    e (LLVMPointerType w) ->
    Alignment ->
    UndefinedBehavior e

  -- -------------------------------- Pointer arithmetic

  PtrAddOffsetOutOfBounds ::
    (1 <= w) =>
    e (LLVMPointerType w) ->
    e (BVType w) ->
    UndefinedBehavior e

  -- | Arguments: kind of comparison, the invalid pointer, the other pointer
  CompareInvalidPointer ::
    (1 <= w) =>
    PtrComparisonOperator ->
    e (LLVMPointerType w) ->
    e (LLVMPointerType w) ->
    UndefinedBehavior e

  -- | "In all other cases, the behavior is undefined"
  -- TODO: 'PtrComparisonOperator' argument?
  CompareDifferentAllocs ::
    (1 <= w) =>
    e (LLVMPointerType w) ->
    e (LLVMPointerType w) ->
    UndefinedBehavior e

  -- | "When two pointers are subtracted, both shall point to elements of the
  -- same array object"
  PtrSubDifferentAllocs ::
    (1 <= w) =>
    e (LLVMPointerType w) ->
    e (LLVMPointerType w) ->
    UndefinedBehavior e

  -- | Pointer cast to an integer type other than
  --   pointer width integers
  PointerIntCast ::
    (1 <= w) =>
    e (LLVMPointerType w) ->
    StorageType ->
    UndefinedBehavior e

  -- | Pointer used in an unsupported arithmetic or bitvector operation
  PointerUnsupportedOp ::
    (1 <= w) =>
    e (LLVMPointerType w) ->
    String ->
    UndefinedBehavior e

  -- | Pointer cast to a floating-point type
  PointerFloatCast ::
    (1 <= w) =>
    e (LLVMPointerType w) ->
    StorageType ->
    UndefinedBehavior e

  -- | "One of the following shall hold: [...] one operand is a pointer and the
  -- other is a null pointer constant."
  ComparePointerToBV ::
    (1 <= w) =>
    e (LLVMPointerType w) ->
    e (BVType w) ->
    UndefinedBehavior e

  -------------------------------- Division operators

  -- | @SymBV@ or @Expr _ _ (BVType w)@
  UDivByZero   :: (1 <= w) => e (BVType w) -> e (BVType w) -> UndefinedBehavior e
  SDivByZero   :: (1 <= w) => e (BVType w) -> e (BVType w) -> UndefinedBehavior e
  URemByZero   :: (1 <= w) => e (BVType w) -> e (BVType w) -> UndefinedBehavior e
  SRemByZero   :: (1 <= w) => e (BVType w) -> e (BVType w) -> UndefinedBehavior e
  SDivOverflow :: (1 <= w) => e (BVType w) -> e (BVType w) -> UndefinedBehavior e
  SRemOverflow :: (1 <= w) => e (BVType w) -> e (BVType w) -> UndefinedBehavior e

  -------------------------------- Integer arithmetic

  AbsIntMin    :: (1 <= w) => e (BVType w) -> UndefinedBehavior e

  PoisonValueCreated ::
    Poison.Poison e ->
    UndefinedBehavior e

  {-
  MemcpyDisjoint          :: UndefinedBehavior e
  DereferenceBadAlignment :: UndefinedBehavior e
  ModifiedStringLiteral   :: UndefinedBehavior e
  -}
  deriving (Typeable)

-- | Which document prohibits this behavior?
standard :: UndefinedBehavior e -> Standard
standard :: forall (e :: CrucibleType -> Type). UndefinedBehavior e -> Standard
standard =
  \case

    -- -------------------------------- Memory management

    DoubleFree{}              -> CStdVer -> Standard
CStd CStdVer
C11
    FreeBadOffset{}           -> CStdVer -> Standard
CStd CStdVer
C11
    FreeUnallocated{}         -> CStdVer -> Standard
CStd CStdVer
C11
    MemsetInvalidRegion{}     -> CStdVer -> Standard
CStd CStdVer
C11
    ReadBadAlignment{}        -> CStdVer -> Standard
CStd CStdVer
C11
    WriteBadAlignment{}       -> CStdVer -> Standard
CStd CStdVer
C11

    -- -------------------------------- Pointer arithmetic

    PtrAddOffsetOutOfBounds{} -> CStdVer -> Standard
CStd CStdVer
C11
    CompareInvalidPointer{}   -> CStdVer -> Standard
CStd CStdVer
C11
    CompareDifferentAllocs{}  -> CStdVer -> Standard
CStd CStdVer
C11
    PtrSubDifferentAllocs{}   -> CStdVer -> Standard
CStd CStdVer
C11
    ComparePointerToBV{}      -> CStdVer -> Standard
CStd CStdVer
C11
    PointerFloatCast{}        -> CStdVer -> Standard
CStd CStdVer
C11
    PointerIntCast{}          -> CStdVer -> Standard
CStd CStdVer
C11
    PointerUnsupportedOp{}    -> CStdVer -> Standard
CStd CStdVer
C11

    -- -------------------------------- Division operators

    UDivByZero{}   -> CStdVer -> Standard
CStd CStdVer
C11
    SDivByZero{}   -> CStdVer -> Standard
CStd CStdVer
C11
    URemByZero{}   -> CStdVer -> Standard
CStd CStdVer
C11
    SRemByZero{}   -> CStdVer -> Standard
CStd CStdVer
C11
    SDivOverflow{} -> CStdVer -> Standard
CStd CStdVer
C11
    SRemOverflow{} -> CStdVer -> Standard
CStd CStdVer
C11

    -- -------------------------------- Integer arithmetic

    AbsIntMin{}    -> CStdVer -> Standard
CStd CStdVer
C11

    PoisonValueCreated Poison e
p -> Poison e -> Standard
forall (e :: CrucibleType -> Type). Poison e -> Standard
Poison.standard Poison e
p

    {-
    MemcpyDisjoint          -> CStd C11
    DereferenceBadAlignment -> CStd C11
    ModifiedStringLiteral   -> CStd C11
    -}

-- | Which section(s) of the document prohibit this behavior?
cite :: UndefinedBehavior e -> Doc ann
cite :: forall (e :: CrucibleType -> Type) ann.
UndefinedBehavior e -> Doc ann
cite =
  \case

    -------------------------------- Memory management

    FreeBadOffset{}           -> Doc ann
"§7.22.3.3 The free function, ¶2"
    FreeUnallocated{}         -> Doc ann
"§7.22.3.3 The free function, ¶2"
    DoubleFree{}              -> Doc ann
"§7.22.3.3 The free function, ¶2"
    MemsetInvalidRegion{}     -> Doc ann
"§7.24.1 String function conventions, ¶1"
    ReadBadAlignment{}        -> Doc ann
"§6.5.3.2 Address and indirection operators, ¶4"
    WriteBadAlignment{}       -> Doc ann
"§6.5.3.2 Address and indirection operators, ¶4"

    ---------------------------------- Pointer arithmetic

    PtrAddOffsetOutOfBounds{} -> Doc ann
"§6.5.6 Additive operators, ¶8"
    CompareInvalidPointer{}   -> Doc ann
"§6.5.8 Relational operators, ¶5"
    CompareDifferentAllocs{}  -> Doc ann
"§6.5.8 Relational operators, ¶5"
    PtrSubDifferentAllocs{}   -> Doc ann
"§6.5.6 Additive operators, ¶9"
    ComparePointerToBV{}      -> Doc ann
"§6.5.9 Equality operators, ¶2"
    PointerFloatCast{}        -> Doc ann
"§6.5.4 Cast operators, ¶4"
    PointerIntCast{}          -> Doc ann
"§6.3.2.3 Conversions, pointers, ¶6"
    PointerUnsupportedOp{}    -> Doc ann
"§6.3.2.3 Conversions, pointers, ¶6"

    -------------------------------- Division operators

    UDivByZero{}   -> Doc ann
"§6.5.5 Multiplicitive operators, ¶5"
    SDivByZero{}   -> Doc ann
"§6.5.5 Multiplicitive operators, ¶5"
    URemByZero{}   -> Doc ann
"§6.5.5 Multiplicitive operators, ¶5"
    SRemByZero{}   -> Doc ann
"§6.5.5 Multiplicitive operators, ¶5"
    SDivOverflow{} -> Doc ann
"§6.5.5 Multiplicitive operators, ¶6"
    SRemOverflow{} -> Doc ann
"§6.5.5 Multiplicitive operators, ¶6"

    -------------------------------- Integer arithmetic

    AbsIntMin{} -> Doc ann
"§7.22.6 Integer arithmetic functions, ¶1"

    PoisonValueCreated Poison e
p -> Poison e -> Doc ann
forall (e :: CrucibleType -> Type) ann. Poison e -> Doc ann
Poison.cite Poison e
p

    -------------------------------- Other

    {-
    MemcpyDisjoint          -> "§7.24.2.1 The memcpy function"
    DereferenceBadAlignment -> "§6.5.3.2 Address and indirection operators"
    ModifiedStringLiteral   -> "§J.2 Undefined behavior" -- 6.4.5
    -}

-- | What happened, and why is it a problem?
--
-- This is a generic explanation that doesn't use the included data.
explain :: UndefinedBehavior e -> Doc ann
explain :: forall (e :: CrucibleType -> Type) ann.
UndefinedBehavior e -> Doc ann
explain =
  \case

    -- -------------------------------- Memory management

    FreeBadOffset e (LLVMPointerType w)
_ -> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
cat ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$
      [ Doc ann
"`free` called on pointer that was not previously returned by `malloc`"
      , Doc ann
"`calloc`, or another memory management function (the pointer did not"
      , Doc ann
"point to the base of an allocation, its offset should be 0)"
      ]
    FreeUnallocated e (LLVMPointerType w)
_ ->
      Doc ann
"`free` called on pointer that didn't point to a live region of the heap"
    DoubleFree{} -> Doc ann
"`free` called on a pointer to already-freed memory"
    MemsetInvalidRegion{} ->
      Doc ann
"Pointer passed to `memset` didn't point to a mutable allocation with enough space"
    WriteBadAlignment e (LLVMPointerType w)
_ Alignment
_ ->
      Doc ann
"Wrote a value into a pointer with insufficent alignment"
    ReadBadAlignment e (LLVMPointerType w)
_ Alignment
_ ->
      Doc ann
"Read a value from a pointer with insufficent alignment"

    -- -------------------------------- Pointer arithmetic

    PtrAddOffsetOutOfBounds e (LLVMPointerType w)
_ e (BVType w)
_ ->
      Doc ann
"Addition of an offset to a pointer resulted in a pointer to an address outside of the allocation"
    CompareInvalidPointer{} ->
      Doc ann
"Comparison of a pointer which wasn't null or a pointer to a live heap object"
    CompareDifferentAllocs e (LLVMPointerType w)
_ e (LLVMPointerType w)
_ ->
      Doc ann
"Comparison of pointers from different allocations"
    PtrSubDifferentAllocs e (LLVMPointerType w)
_ e (LLVMPointerType w)
_ ->
      Doc ann
"Subtraction of pointers from different allocations"
    ComparePointerToBV e (LLVMPointerType w)
_ e (BVType w)
_ ->
      Doc ann
"Comparison of a pointer to a non zero (null) integer value"
    PointerFloatCast{} ->
      Doc ann
"Cast of a pointer to a floating-point type"
    PointerIntCast{} ->
      Doc ann
"Cast of a pointer to an incompatible integer type"
    PointerUnsupportedOp{} ->
      Doc ann
"Pointer cast to an integer used in an unsupported operation"

    -------------------------------- Division operators

    UDivByZero{}   -> Doc ann
"Unsigned division by zero"
    SDivByZero{}   -> Doc ann
"Signed division by zero"
    URemByZero{}   -> Doc ann
"Unsigned division by zero via remainder"
    SRemByZero{}   -> Doc ann
"Signed division by zero via remainder"
    SDivOverflow{} -> Doc ann
"Overflow during signed division"
    SRemOverflow{} -> Doc ann
"Overflow during signed division (via signed remainder)"

    -------------------------------- Integer arithmetic

    AbsIntMin{} -> Doc ann
"`abs`, `labs`, or `llabs` called on `INT_MIN`"

    PoisonValueCreated Poison e
p -> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [ Doc ann
"Poison value created", Poison e -> Doc ann
forall (e :: CrucibleType -> Type) ann. Poison e -> Doc ann
Poison.explain Poison e
p ]

    -------------------------------- Other

    {-
    MemcpyDisjoint     -> "Use of `memcpy` with non-disjoint regions of memory"
    DereferenceBadAlignment ->
      "Dereferenced a pointer to a type with the wrong alignment"
    ModifiedStringLiteral -> "Modified the underlying array of a string literal"
    -}

-- | Pretty-print the additional information held by the constructors
-- (for symbolic expressions)
details :: W4I.IsExpr (W4I.SymExpr sym)
        => UndefinedBehavior (RegValue' sym)
        -> [Doc ann]
details :: forall sym ann.
IsExpr (SymExpr sym) =>
UndefinedBehavior (RegValue' sym) -> [Doc ann]
details =
  \case

    -------------------------------- Memory management

    FreeBadOffset RegValue' sym (LLVMPointerType w)
ptr   -> [ RegValue' sym (LLVMPointerType w) -> Doc ann
forall sym (w :: Natural) ann.
IsExpr (SymExpr sym) =>
RegValue' sym (LLVMPointerType w) -> Doc ann
ppPtr1 RegValue' sym (LLVMPointerType w)
ptr ]
    FreeUnallocated RegValue' sym (LLVMPointerType w)
ptr -> [ RegValue' sym (LLVMPointerType w) -> Doc ann
forall sym (w :: Natural) ann.
IsExpr (SymExpr sym) =>
RegValue' sym (LLVMPointerType w) -> Doc ann
ppPtr1 RegValue' sym (LLVMPointerType w)
ptr ]
    DoubleFree RegValue' sym (LLVMPointerType w)
ptr -> [ RegValue' sym (LLVMPointerType w) -> Doc ann
forall sym (w :: Natural) ann.
IsExpr (SymExpr sym) =>
RegValue' sym (LLVMPointerType w) -> Doc ann
ppPtr1 RegValue' sym (LLVMPointerType w)
ptr ]
    MemsetInvalidRegion RegValue' sym (LLVMPointerType w)
destPtr RegValue' sym (BVType 8)
fillByte RegValue' sym (BVType v)
len ->
      [ Doc ann
"Destination pointer:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> RegValue' sym (LLVMPointerType w) -> Doc ann
forall sym (w :: Natural) ann.
IsExpr (SymExpr sym) =>
RegValue' sym (LLVMPointerType w) -> Doc ann
ppPtr1 RegValue' sym (LLVMPointerType w)
destPtr
      , Doc ann
"Fill byte:          " Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> (SymExpr sym ('BaseBVType 8) -> Doc ann
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
W4I.printSymExpr (SymExpr sym ('BaseBVType 8) -> Doc ann)
-> SymExpr sym ('BaseBVType 8) -> Doc ann
forall a b. (a -> b) -> a -> b
$ RegValue' sym (BVType 8) -> RegValue sym (BVType 8)
forall sym (tp :: CrucibleType).
RegValue' sym tp -> RegValue sym tp
unRV RegValue' sym (BVType 8)
fillByte)
      , Doc ann
"Length:             " Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> (SymExpr sym ('BaseBVType v) -> Doc ann
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
W4I.printSymExpr (SymExpr sym ('BaseBVType v) -> Doc ann)
-> SymExpr sym ('BaseBVType v) -> Doc ann
forall a b. (a -> b) -> a -> b
$ RegValue' sym (BVType v) -> RegValue sym (BVType v)
forall sym (tp :: CrucibleType).
RegValue' sym tp -> RegValue sym tp
unRV RegValue' sym (BVType v)
len)
      ]
    WriteBadAlignment RegValue' sym (LLVMPointerType w)
ptr Alignment
alignment ->
      -- TODO: replace viaShow when we have instance Pretty Bytes
      [ Doc ann
"Required alignment:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Bytes -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow (Alignment -> Bytes
fromAlignment Alignment
alignment) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"bytes"
      , RegValue' sym (LLVMPointerType w) -> Doc ann
forall sym (w :: Natural) ann.
IsExpr (SymExpr sym) =>
RegValue' sym (LLVMPointerType w) -> Doc ann
ppPtr1 RegValue' sym (LLVMPointerType w)
ptr
      ]
    ReadBadAlignment RegValue' sym (LLVMPointerType w)
ptr Alignment
alignment ->
      -- TODO: replace viaShow when we have instance Pretty Bytes
      [ Doc ann
"Required alignment:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Bytes -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow (Alignment -> Bytes
fromAlignment Alignment
alignment) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"bytes"
      , RegValue' sym (LLVMPointerType w) -> Doc ann
forall sym (w :: Natural) ann.
IsExpr (SymExpr sym) =>
RegValue' sym (LLVMPointerType w) -> Doc ann
ppPtr1 RegValue' sym (LLVMPointerType w)
ptr
      ]

    -------------------------------- Pointer arithmetic

    PtrAddOffsetOutOfBounds RegValue' sym (LLVMPointerType w)
ptr RegValue' sym (BVType w)
offset ->
      [ RegValue' sym (LLVMPointerType w) -> Doc ann
forall sym (w :: Natural) ann.
IsExpr (SymExpr sym) =>
RegValue' sym (LLVMPointerType w) -> Doc ann
ppPtr1 RegValue' sym (LLVMPointerType w)
ptr
      , SymExpr sym (BaseBVType w) -> Doc ann
forall (e :: BaseType -> Type) (w :: Natural) ann.
IsExpr e =>
e (BaseBVType w) -> Doc ann
ppOffset (RegValue' sym (BVType w) -> RegValue sym (BVType w)
forall sym (tp :: CrucibleType).
RegValue' sym tp -> RegValue sym tp
unRV RegValue' sym (BVType w)
offset)
      ]
    CompareInvalidPointer PtrComparisonOperator
comparison RegValue' sym (LLVMPointerType w)
invalid RegValue' sym (LLVMPointerType w)
other ->
      [ Doc ann
"Comparison:                    " Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> PtrComparisonOperator -> Doc ann
forall ann. PtrComparisonOperator -> Doc ann
ppPtrComparison PtrComparisonOperator
comparison
      , Doc ann
"Invalid pointer:               " Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> LLVMPtr sym w -> Doc ann
forall sym (wptr :: Natural) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
ppPtr (RegValue' sym (LLVMPointerType w) -> LLVMPtr sym w
forall sym (tp :: CrucibleType).
RegValue' sym tp -> RegValue sym tp
unRV RegValue' sym (LLVMPointerType w)
invalid)
      , Doc ann
"Other (possibly valid) pointer:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> LLVMPtr sym w -> Doc ann
forall sym (wptr :: Natural) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
ppPtr (RegValue' sym (LLVMPointerType w) -> LLVMPtr sym w
forall sym (tp :: CrucibleType).
RegValue' sym tp -> RegValue sym tp
unRV RegValue' sym (LLVMPointerType w)
other)
      ]
    CompareDifferentAllocs RegValue' sym (LLVMPointerType w)
ptr1 RegValue' sym (LLVMPointerType w)
ptr2 -> [ RegValue' sym (LLVMPointerType w)
-> RegValue' sym (LLVMPointerType w) -> Doc ann
forall {sym} {tp :: CrucibleType} {sym} {wptr :: Natural} {sym}
       {tp :: CrucibleType} {sym} {wptr :: Natural} {ann}.
(RegValue sym tp ~ LLVMPointer sym wptr,
 RegValue sym tp ~ LLVMPointer sym wptr, IsExpr (SymExpr sym),
 IsExpr (SymExpr sym)) =>
RegValue' sym tp -> RegValue' sym tp -> Doc ann
ppPtr2 RegValue' sym (LLVMPointerType w)
ptr1 RegValue' sym (LLVMPointerType w)
ptr2 ]
    PtrSubDifferentAllocs RegValue' sym (LLVMPointerType w)
ptr1 RegValue' sym (LLVMPointerType w)
ptr2  -> [ RegValue' sym (LLVMPointerType w)
-> RegValue' sym (LLVMPointerType w) -> Doc ann
forall {sym} {tp :: CrucibleType} {sym} {wptr :: Natural} {sym}
       {tp :: CrucibleType} {sym} {wptr :: Natural} {ann}.
(RegValue sym tp ~ LLVMPointer sym wptr,
 RegValue sym tp ~ LLVMPointer sym wptr, IsExpr (SymExpr sym),
 IsExpr (SymExpr sym)) =>
RegValue' sym tp -> RegValue' sym tp -> Doc ann
ppPtr2 RegValue' sym (LLVMPointerType w)
ptr1 RegValue' sym (LLVMPointerType w)
ptr2 ]
    ComparePointerToBV RegValue' sym (LLVMPointerType w)
ptr RegValue' sym (BVType w)
bv ->
      [ RegValue' sym (LLVMPointerType w) -> Doc ann
forall sym (w :: Natural) ann.
IsExpr (SymExpr sym) =>
RegValue' sym (LLVMPointerType w) -> Doc ann
ppPtr1 RegValue' sym (LLVMPointerType w)
ptr
      , Doc ann
"Bitvector:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> (SymExpr sym ('BaseBVType w) -> Doc ann
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
W4I.printSymExpr (SymExpr sym ('BaseBVType w) -> Doc ann)
-> SymExpr sym ('BaseBVType w) -> Doc ann
forall a b. (a -> b) -> a -> b
$ RegValue' sym (BVType w) -> RegValue sym (BVType w)
forall sym (tp :: CrucibleType).
RegValue' sym tp -> RegValue sym tp
unRV RegValue' sym (BVType w)
bv)
      ]
    PointerFloatCast RegValue' sym (LLVMPointerType w)
ptr StorageType
castType ->
      [ RegValue' sym (LLVMPointerType w) -> Doc ann
forall sym (w :: Natural) ann.
IsExpr (SymExpr sym) =>
RegValue' sym (LLVMPointerType w) -> Doc ann
ppPtr1 RegValue' sym (LLVMPointerType w)
ptr
      , Doc ann
"Cast to:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> StorageType -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow StorageType
castType
      ]
    PointerIntCast RegValue' sym (LLVMPointerType w)
ptr StorageType
castType ->
      [ RegValue' sym (LLVMPointerType w) -> Doc ann
forall sym (w :: Natural) ann.
IsExpr (SymExpr sym) =>
RegValue' sym (LLVMPointerType w) -> Doc ann
ppPtr1 RegValue' sym (LLVMPointerType w)
ptr
      , Doc ann
"Cast to:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> StorageType -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow StorageType
castType
      ]
    PointerUnsupportedOp RegValue' sym (LLVMPointerType w)
ptr [Char]
msg ->
      [ RegValue' sym (LLVMPointerType w) -> Doc ann
forall sym (w :: Natural) ann.
IsExpr (SymExpr sym) =>
RegValue' sym (LLVMPointerType w) -> Doc ann
ppPtr1 RegValue' sym (LLVMPointerType w)
ptr
      , [Char] -> Doc ann
forall ann. [Char] -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [Char]
msg
      ]

    -------------------------------- Division operators

    -- The cases are manually listed to prevent unintentional fallthrough if a
    -- constructor is added.
    UDivByZero RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2   -> [ RegValue' sym (BVType w) -> RegValue' sym (BVType w) -> Doc ann
forall sym (w :: Natural) ann.
IsExpr (SymExpr sym) =>
RegValue' sym (BVType w) -> RegValue' sym (BVType w) -> Doc ann
ppBV2 RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ]
    SDivByZero RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2   -> [ RegValue' sym (BVType w) -> RegValue' sym (BVType w) -> Doc ann
forall sym (w :: Natural) ann.
IsExpr (SymExpr sym) =>
RegValue' sym (BVType w) -> RegValue' sym (BVType w) -> Doc ann
ppBV2 RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ]
    URemByZero RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2   -> [ RegValue' sym (BVType w) -> RegValue' sym (BVType w) -> Doc ann
forall sym (w :: Natural) ann.
IsExpr (SymExpr sym) =>
RegValue' sym (BVType w) -> RegValue' sym (BVType w) -> Doc ann
ppBV2 RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ]
    SRemByZero RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2   -> [ RegValue' sym (BVType w) -> RegValue' sym (BVType w) -> Doc ann
forall sym (w :: Natural) ann.
IsExpr (SymExpr sym) =>
RegValue' sym (BVType w) -> RegValue' sym (BVType w) -> Doc ann
ppBV2 RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ]
    SDivOverflow RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 -> [ RegValue' sym (BVType w) -> RegValue' sym (BVType w) -> Doc ann
forall sym (w :: Natural) ann.
IsExpr (SymExpr sym) =>
RegValue' sym (BVType w) -> RegValue' sym (BVType w) -> Doc ann
ppBV2 RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ]
    SRemOverflow RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 -> [ RegValue' sym (BVType w) -> RegValue' sym (BVType w) -> Doc ann
forall sym (w :: Natural) ann.
IsExpr (SymExpr sym) =>
RegValue' sym (BVType w) -> RegValue' sym (BVType w) -> Doc ann
ppBV2 RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ]

    -------------------------------- Integer arithmetic

    AbsIntMin RegValue' sym (BVType w)
v -> [ RegValue' sym (BVType w) -> Doc ann
forall sym (w :: Natural) ann.
IsExpr (SymExpr sym) =>
RegValue' sym (BVType w) -> Doc ann
ppBV1 RegValue' sym (BVType w)
v ]

    PoisonValueCreated Poison (RegValue' sym)
p -> Poison (RegValue' sym) -> [Doc ann]
forall sym ann.
IsExpr (SymExpr sym) =>
Poison (RegValue' sym) -> [Doc ann]
Poison.details Poison (RegValue' sym)
p

  where ppBV1 :: W4I.IsExpr (W4I.SymExpr sym) =>
                 RegValue' sym (BVType w) -> Doc ann
        ppBV1 :: forall sym (w :: Natural) ann.
IsExpr (SymExpr sym) =>
RegValue' sym (BVType w) -> Doc ann
ppBV1 (RV RegValue sym (BVType w)
bv) = Doc ann
"op:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> SymExpr sym ('BaseBVType w) -> Doc ann
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
W4I.printSymExpr RegValue sym (BVType w)
SymExpr sym ('BaseBVType w)
bv

        ppBV2 :: W4I.IsExpr (W4I.SymExpr sym) =>
                 RegValue' sym (BVType w) -> RegValue' sym (BVType w) -> Doc ann
        ppBV2 :: forall sym (w :: Natural) ann.
IsExpr (SymExpr sym) =>
RegValue' sym (BVType w) -> RegValue' sym (BVType w) -> Doc ann
ppBV2 (RV RegValue sym (BVType w)
bv1) (RV RegValue sym (BVType w)
bv2) =
          [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [ Doc ann
"op1: " Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> SymExpr sym ('BaseBVType w) -> Doc ann
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
W4I.printSymExpr RegValue sym (BVType w)
SymExpr sym ('BaseBVType w)
bv1
               , Doc ann
"op2: " Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> SymExpr sym ('BaseBVType w) -> Doc ann
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
W4I.printSymExpr RegValue sym (BVType w)
SymExpr sym ('BaseBVType w)
bv2
               ]

        ppPtr1 :: W4I.IsExpr (W4I.SymExpr sym) => RegValue' sym (LLVMPointerType w) -> Doc ann
        ppPtr1 :: forall sym (w :: Natural) ann.
IsExpr (SymExpr sym) =>
RegValue' sym (LLVMPointerType w) -> Doc ann
ppPtr1 (RV RegValue sym (LLVMPointerType w)
p) = Doc ann
"Pointer:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> RegValue sym (LLVMPointerType w) -> Doc ann
forall sym (wptr :: Natural) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
ppPtr RegValue sym (LLVMPointerType w)
p

        ppPtr2 :: RegValue' sym tp -> RegValue' sym tp -> Doc ann
ppPtr2 (RV RegValue sym tp
ptr1) (RV RegValue sym tp
ptr2) =
          [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat [ Doc ann
"Pointer 1:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+>  LLVMPtr sym wptr -> Doc ann
forall sym (wptr :: Natural) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
ppPtr RegValue sym tp
LLVMPtr sym wptr
ptr1
               , Doc ann
"Pointer 2:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+>  LLVMPtr sym wptr -> Doc ann
forall sym (wptr :: Natural) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
ppPtr RegValue sym tp
LLVMPtr sym wptr
ptr2
               ]

        ppOffset :: W4I.IsExpr e => e (BaseBVType w) -> Doc ann
        ppOffset :: forall (e :: BaseType -> Type) (w :: Natural) ann.
IsExpr e =>
e (BaseBVType w) -> Doc ann
ppOffset = (Doc ann
"Offset:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+>) (Doc ann -> Doc ann)
-> (e (BaseBVType w) -> Doc ann) -> e (BaseBVType w) -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e (BaseBVType w) -> Doc ann
forall (tp :: BaseType) ann. e tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
W4I.printSymExpr

pp :: (UndefinedBehavior e -> [Doc ann]) -- ^ Printer for constructor data
   -> UndefinedBehavior e
   -> Doc ann
pp :: forall (e :: CrucibleType -> Type) ann.
(UndefinedBehavior e -> [Doc ann])
-> UndefinedBehavior e -> Doc ann
pp UndefinedBehavior e -> [Doc ann]
extra UndefinedBehavior e
ub = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat (UndefinedBehavior e -> Doc ann
forall (e :: CrucibleType -> Type) ann.
UndefinedBehavior e -> Doc ann
explain UndefinedBehavior e
ub Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: UndefinedBehavior e -> [Doc ann]
extra UndefinedBehavior e
ub [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ UndefinedBehavior e -> [Doc ann]
forall (e :: CrucibleType -> Type) ann.
UndefinedBehavior e -> [Doc ann]
ppCitation UndefinedBehavior e
ub)

-- | Pretty-printer for symbolic backends
ppDetails ::
  W4I.IsExpr (W4I.SymExpr sym) =>
  UndefinedBehavior (RegValue' sym) ->
  Doc ann
ppDetails :: forall sym ann.
IsExpr (SymExpr sym) =>
UndefinedBehavior (RegValue' sym) -> Doc ann
ppDetails UndefinedBehavior (RegValue' sym)
ub = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat (UndefinedBehavior (RegValue' sym) -> [Doc ann]
forall sym ann.
IsExpr (SymExpr sym) =>
UndefinedBehavior (RegValue' sym) -> [Doc ann]
details UndefinedBehavior (RegValue' sym)
ub [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ UndefinedBehavior (RegValue' sym) -> [Doc ann]
forall (e :: CrucibleType -> Type) ann.
UndefinedBehavior e -> [Doc ann]
ppCitation UndefinedBehavior (RegValue' sym)
ub)

ppCitation :: UndefinedBehavior e -> [Doc ann]
ppCitation :: forall (e :: CrucibleType -> Type) ann.
UndefinedBehavior e -> [Doc ann]
ppCitation UndefinedBehavior e
ub =
   ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
cat [ Doc ann
"Reference: "
        , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Standard -> Text
ppStd (UndefinedBehavior e -> Standard
forall (e :: CrucibleType -> Type). UndefinedBehavior e -> Standard
standard UndefinedBehavior e
ub)))
        , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (UndefinedBehavior e -> Doc ann
forall (e :: CrucibleType -> Type) ann.
UndefinedBehavior e -> Doc ann
cite UndefinedBehavior e
ub)
        ]
    Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: case Standard -> Maybe Text
stdURL (UndefinedBehavior e -> Standard
forall (e :: CrucibleType -> Type). UndefinedBehavior e -> Standard
standard UndefinedBehavior e
ub) of
        Just Text
url -> [ Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Doc ann
"Document URL:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
url) ]
        Maybe Text
Nothing  -> [])

-- -----------------------------------------------------------------------
-- ** Instances

$(return [])

instance TestEqualityC UndefinedBehavior where
  testEqualityC :: forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
 f x -> f y -> Maybe (x :~: y))
-> UndefinedBehavior f -> UndefinedBehavior f -> Bool
testEqualityC forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> Maybe (x :~: y)
subterms UndefinedBehavior f
x UndefinedBehavior f
y = Maybe (Any :~: Any) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Any :~: Any) -> Bool) -> Maybe (Any :~: Any) -> Bool
forall a b. (a -> b) -> a -> b
$
    $(U.structuralTypeEquality [t|UndefinedBehavior|]
       [ ( U.DataArg 0 `U.TypeApp` U.AnyType
         , [| subterms |]
         )
       , ( U.ConType [t|Poison.Poison|] `U.TypeApp` U.AnyType
         , [| \a b -> if testEqualityC subterms a b then Just Refl else Nothing |]
         )
       ]
     ) UndefinedBehavior f
x UndefinedBehavior f
y

instance OrdC UndefinedBehavior where
  compareC :: forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
 f x -> g y -> OrderingF x y)
-> UndefinedBehavior f -> UndefinedBehavior g -> Ordering
compareC forall (x :: CrucibleType) (y :: CrucibleType).
f x -> g y -> OrderingF x y
subterms UndefinedBehavior f
ub1 UndefinedBehavior g
ub2 = OrderingF Any Any -> Ordering
forall {k} (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (OrderingF Any Any -> Ordering) -> OrderingF Any Any -> Ordering
forall a b. (a -> b) -> a -> b
$
    $(U.structuralTypeOrd [t|UndefinedBehavior|]
       [ ( U.DataArg 0 `U.TypeApp` U.AnyType
         , [| subterms |]
         )
       , ( U.ConType [t|Poison.Poison|] `U.TypeApp` U.AnyType
         , [| \a b -> fromOrdering (compareC subterms a b) |]
         )
       ]
     ) UndefinedBehavior f
ub1 UndefinedBehavior g
ub2

instance FunctorF UndefinedBehavior where
  fmapF :: forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x)
-> UndefinedBehavior f -> UndefinedBehavior g
fmapF = (forall (s :: CrucibleType). f s -> g s)
-> UndefinedBehavior f -> UndefinedBehavior g
forall {k} (t :: (k -> Type) -> Type) (e :: k -> Type)
       (f :: k -> Type).
TraversableF t =>
(forall (s :: k). e s -> f s) -> t e -> t f
TF.fmapFDefault

instance FoldableF UndefinedBehavior where
  foldMapF :: forall m (e :: CrucibleType -> Type).
Monoid m =>
(forall (s :: CrucibleType). e s -> m) -> UndefinedBehavior e -> m
foldMapF = (forall (s :: CrucibleType). e s -> m) -> UndefinedBehavior e -> m
forall {k} (t :: (k -> Type) -> Type) m (e :: k -> Type).
(TraversableF t, Monoid m) =>
(forall (s :: k). e s -> m) -> t e -> m
TF.foldMapFDefault

instance TraversableF UndefinedBehavior where
  traverseF :: forall (m :: Type -> Type) (e :: CrucibleType -> Type)
       (f :: CrucibleType -> Type).
Applicative m =>
(forall (s :: CrucibleType). e s -> m (f s))
-> UndefinedBehavior e -> m (UndefinedBehavior f)
traverseF forall (s :: CrucibleType). e s -> m (f s)
subterms =
    $(U.structuralTraversal [t|UndefinedBehavior|]
       [ ( U.DataArg 0 `U.TypeApp` U.AnyType
         , [| \_ x -> subterms x |]
         )
       , ( U.ConType [t|Poison.Poison|] `U.TypeApp` U.AnyType
         , [| \_ x -> traverseF subterms x |]
         )
       ]
     ) e Any -> m (f Any)
forall (s :: CrucibleType). e s -> m (f s)
subterms


concUB :: forall sym.
  W4I.IsExprBuilder sym =>
  sym ->
  (forall tp. W4I.SymExpr sym tp -> IO (GroundValue tp)) ->
  UndefinedBehavior (RegValue' sym) -> IO (UndefinedBehavior (RegValue' sym))
concUB :: forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> UndefinedBehavior (RegValue' sym)
-> IO (UndefinedBehavior (RegValue' sym))
concUB sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc UndefinedBehavior (RegValue' sym)
ub =
  let bv :: forall w. (1 <= w) => RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
      bv :: forall (w :: Natural).
(1 <= w) =>
RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
bv (RV RegValue sym (BVType w)
x) = RegValue sym (BVType w) -> RegValue' sym (BVType w)
SymExpr sym ('BaseBVType w) -> RegValue' sym (BVType w)
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
RV (SymExpr sym ('BaseBVType w) -> RegValue' sym (BVType w))
-> IO (SymExpr sym ('BaseBVType w))
-> IO (RegValue' sym (BVType w))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> SymExpr sym ('BaseBVType w)
-> IO (SymExpr sym ('BaseBVType w))
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> SymBV sym w
-> IO (SymBV sym w)
concBV sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc RegValue sym (BVType w)
SymExpr sym ('BaseBVType w)
x in
  case UndefinedBehavior (RegValue' sym)
ub of
    FreeBadOffset RegValue' sym (LLVMPointerType w)
ptr ->
      RegValue' sym (LLVMPointerType w)
-> UndefinedBehavior (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (LLVMPointerType w) -> UndefinedBehavior e
FreeBadOffset (RegValue' sym (LLVMPointerType w)
 -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (LLVMPointerType w))
-> IO (UndefinedBehavior (RegValue' sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
concPtr' sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc RegValue' sym (LLVMPointerType w)
ptr
    FreeUnallocated RegValue' sym (LLVMPointerType w)
ptr ->
      RegValue' sym (LLVMPointerType w)
-> UndefinedBehavior (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (LLVMPointerType w) -> UndefinedBehavior e
FreeUnallocated (RegValue' sym (LLVMPointerType w)
 -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (LLVMPointerType w))
-> IO (UndefinedBehavior (RegValue' sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
concPtr' sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc RegValue' sym (LLVMPointerType w)
ptr
    DoubleFree RegValue' sym (LLVMPointerType w)
ptr ->
      RegValue' sym (LLVMPointerType w)
-> UndefinedBehavior (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (LLVMPointerType w) -> UndefinedBehavior e
DoubleFree (RegValue' sym (LLVMPointerType w)
 -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (LLVMPointerType w))
-> IO (UndefinedBehavior (RegValue' sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
concPtr' sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc RegValue' sym (LLVMPointerType w)
ptr
    MemsetInvalidRegion RegValue' sym (LLVMPointerType w)
ptr RegValue' sym (BVType 8)
val RegValue' sym (BVType v)
len ->
      RegValue' sym (LLVMPointerType w)
-> RegValue' sym (BVType 8)
-> RegValue' sym (BVType v)
-> UndefinedBehavior (RegValue' sym)
forall (w :: Natural) (v :: Natural) (e :: CrucibleType -> Type).
(1 <= w, 1 <= v) =>
e (LLVMPointerType w)
-> e (BVType 8) -> e (BVType v) -> UndefinedBehavior e
MemsetInvalidRegion (RegValue' sym (LLVMPointerType w)
 -> RegValue' sym (BVType 8)
 -> RegValue' sym (BVType v)
 -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (LLVMPointerType w))
-> IO
     (RegValue' sym (BVType 8)
      -> RegValue' sym (BVType v) -> UndefinedBehavior (RegValue' sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
concPtr' sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc RegValue' sym (LLVMPointerType w)
ptr IO
  (RegValue' sym (BVType 8)
   -> RegValue' sym (BVType v) -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (BVType 8))
-> IO
     (RegValue' sym (BVType v) -> UndefinedBehavior (RegValue' sym))
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> RegValue' sym (BVType 8) -> IO (RegValue' sym (BVType 8))
forall (w :: Natural).
(1 <= w) =>
RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
bv RegValue' sym (BVType 8)
val IO (RegValue' sym (BVType v) -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (BVType v))
-> IO (UndefinedBehavior (RegValue' sym))
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> RegValue' sym (BVType v) -> IO (RegValue' sym (BVType v))
forall (w :: Natural).
(1 <= w) =>
RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
bv RegValue' sym (BVType v)
len
    ReadBadAlignment RegValue' sym (LLVMPointerType w)
ptr Alignment
a ->
      RegValue' sym (LLVMPointerType w)
-> Alignment -> UndefinedBehavior (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (LLVMPointerType w) -> Alignment -> UndefinedBehavior e
ReadBadAlignment (RegValue' sym (LLVMPointerType w)
 -> Alignment -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (LLVMPointerType w))
-> IO (Alignment -> UndefinedBehavior (RegValue' sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
concPtr' sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc RegValue' sym (LLVMPointerType w)
ptr IO (Alignment -> UndefinedBehavior (RegValue' sym))
-> IO Alignment -> IO (UndefinedBehavior (RegValue' sym))
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Alignment -> IO Alignment
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Alignment
a
    WriteBadAlignment RegValue' sym (LLVMPointerType w)
ptr Alignment
a ->
      RegValue' sym (LLVMPointerType w)
-> Alignment -> UndefinedBehavior (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (LLVMPointerType w) -> Alignment -> UndefinedBehavior e
WriteBadAlignment (RegValue' sym (LLVMPointerType w)
 -> Alignment -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (LLVMPointerType w))
-> IO (Alignment -> UndefinedBehavior (RegValue' sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
concPtr' sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc RegValue' sym (LLVMPointerType w)
ptr IO (Alignment -> UndefinedBehavior (RegValue' sym))
-> IO Alignment -> IO (UndefinedBehavior (RegValue' sym))
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Alignment -> IO Alignment
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Alignment
a

    PtrAddOffsetOutOfBounds RegValue' sym (LLVMPointerType w)
ptr RegValue' sym (BVType w)
off ->
      RegValue' sym (LLVMPointerType w)
-> RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (LLVMPointerType w) -> e (BVType w) -> UndefinedBehavior e
PtrAddOffsetOutOfBounds (RegValue' sym (LLVMPointerType w)
 -> RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (LLVMPointerType w))
-> IO
     (RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
concPtr' sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc RegValue' sym (LLVMPointerType w)
ptr IO (RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO (UndefinedBehavior (RegValue' sym))
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
forall (w :: Natural).
(1 <= w) =>
RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
bv RegValue' sym (BVType w)
off
    CompareInvalidPointer PtrComparisonOperator
op RegValue' sym (LLVMPointerType w)
p1 RegValue' sym (LLVMPointerType w)
p2 ->
      PtrComparisonOperator
-> RegValue' sym (LLVMPointerType w)
-> RegValue' sym (LLVMPointerType w)
-> UndefinedBehavior (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
PtrComparisonOperator
-> e (LLVMPointerType w)
-> e (LLVMPointerType w)
-> UndefinedBehavior e
CompareInvalidPointer PtrComparisonOperator
op (RegValue' sym (LLVMPointerType w)
 -> RegValue' sym (LLVMPointerType w)
 -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (LLVMPointerType w))
-> IO
     (RegValue' sym (LLVMPointerType w)
      -> UndefinedBehavior (RegValue' sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
concPtr' sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc RegValue' sym (LLVMPointerType w)
p1 IO
  (RegValue' sym (LLVMPointerType w)
   -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (LLVMPointerType w))
-> IO (UndefinedBehavior (RegValue' sym))
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
concPtr' sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc RegValue' sym (LLVMPointerType w)
p2
    CompareDifferentAllocs RegValue' sym (LLVMPointerType w)
p1 RegValue' sym (LLVMPointerType w)
p2 ->
      RegValue' sym (LLVMPointerType w)
-> RegValue' sym (LLVMPointerType w)
-> UndefinedBehavior (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (LLVMPointerType w)
-> e (LLVMPointerType w) -> UndefinedBehavior e
CompareDifferentAllocs (RegValue' sym (LLVMPointerType w)
 -> RegValue' sym (LLVMPointerType w)
 -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (LLVMPointerType w))
-> IO
     (RegValue' sym (LLVMPointerType w)
      -> UndefinedBehavior (RegValue' sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
concPtr' sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc RegValue' sym (LLVMPointerType w)
p1 IO
  (RegValue' sym (LLVMPointerType w)
   -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (LLVMPointerType w))
-> IO (UndefinedBehavior (RegValue' sym))
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
concPtr' sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc RegValue' sym (LLVMPointerType w)
p2
    PtrSubDifferentAllocs RegValue' sym (LLVMPointerType w)
p1 RegValue' sym (LLVMPointerType w)
p2 ->
      RegValue' sym (LLVMPointerType w)
-> RegValue' sym (LLVMPointerType w)
-> UndefinedBehavior (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (LLVMPointerType w)
-> e (LLVMPointerType w) -> UndefinedBehavior e
PtrSubDifferentAllocs (RegValue' sym (LLVMPointerType w)
 -> RegValue' sym (LLVMPointerType w)
 -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (LLVMPointerType w))
-> IO
     (RegValue' sym (LLVMPointerType w)
      -> UndefinedBehavior (RegValue' sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
concPtr' sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc RegValue' sym (LLVMPointerType w)
p1 IO
  (RegValue' sym (LLVMPointerType w)
   -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (LLVMPointerType w))
-> IO (UndefinedBehavior (RegValue' sym))
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
concPtr' sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc RegValue' sym (LLVMPointerType w)
p2
    PointerFloatCast RegValue' sym (LLVMPointerType w)
ptr StorageType
tp ->
      RegValue' sym (LLVMPointerType w)
-> StorageType -> UndefinedBehavior (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (LLVMPointerType w) -> StorageType -> UndefinedBehavior e
PointerFloatCast (RegValue' sym (LLVMPointerType w)
 -> StorageType -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (LLVMPointerType w))
-> IO (StorageType -> UndefinedBehavior (RegValue' sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
concPtr' sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc RegValue' sym (LLVMPointerType w)
ptr IO (StorageType -> UndefinedBehavior (RegValue' sym))
-> IO StorageType -> IO (UndefinedBehavior (RegValue' sym))
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> StorageType -> IO StorageType
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure StorageType
tp
    PointerIntCast RegValue' sym (LLVMPointerType w)
ptr StorageType
tp ->
      RegValue' sym (LLVMPointerType w)
-> StorageType -> UndefinedBehavior (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (LLVMPointerType w) -> StorageType -> UndefinedBehavior e
PointerIntCast (RegValue' sym (LLVMPointerType w)
 -> StorageType -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (LLVMPointerType w))
-> IO (StorageType -> UndefinedBehavior (RegValue' sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
concPtr' sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc RegValue' sym (LLVMPointerType w)
ptr IO (StorageType -> UndefinedBehavior (RegValue' sym))
-> IO StorageType -> IO (UndefinedBehavior (RegValue' sym))
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> StorageType -> IO StorageType
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure StorageType
tp
    PointerUnsupportedOp RegValue' sym (LLVMPointerType w)
ptr [Char]
msg ->
      RegValue' sym (LLVMPointerType w)
-> [Char] -> UndefinedBehavior (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (LLVMPointerType w) -> [Char] -> UndefinedBehavior e
PointerUnsupportedOp (RegValue' sym (LLVMPointerType w)
 -> [Char] -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (LLVMPointerType w))
-> IO ([Char] -> UndefinedBehavior (RegValue' sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
concPtr' sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc RegValue' sym (LLVMPointerType w)
ptr IO ([Char] -> UndefinedBehavior (RegValue' sym))
-> IO [Char] -> IO (UndefinedBehavior (RegValue' sym))
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> [Char] -> IO [Char]
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure [Char]
msg
    ComparePointerToBV RegValue' sym (LLVMPointerType w)
ptr RegValue' sym (BVType w)
val ->
      RegValue' sym (LLVMPointerType w)
-> RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (LLVMPointerType w) -> e (BVType w) -> UndefinedBehavior e
ComparePointerToBV (RegValue' sym (LLVMPointerType w)
 -> RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (LLVMPointerType w))
-> IO
     (RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
concPtr' sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc RegValue' sym (LLVMPointerType w)
ptr IO (RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO (UndefinedBehavior (RegValue' sym))
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
forall (w :: Natural).
(1 <= w) =>
RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
bv RegValue' sym (BVType w)
val
    UDivByZero RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ->
      RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> e (BVType w) -> UndefinedBehavior e
UDivByZero (RegValue' sym (BVType w)
 -> RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO
     (RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
forall (w :: Natural).
(1 <= w) =>
RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
bv RegValue' sym (BVType w)
v1 IO (RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO (UndefinedBehavior (RegValue' sym))
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
forall (w :: Natural).
(1 <= w) =>
RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
bv RegValue' sym (BVType w)
v2
    SDivByZero RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ->
      RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> e (BVType w) -> UndefinedBehavior e
SDivByZero (RegValue' sym (BVType w)
 -> RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO
     (RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
forall (w :: Natural).
(1 <= w) =>
RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
bv RegValue' sym (BVType w)
v1 IO (RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO (UndefinedBehavior (RegValue' sym))
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
forall (w :: Natural).
(1 <= w) =>
RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
bv RegValue' sym (BVType w)
v2
    URemByZero RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ->
      RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> e (BVType w) -> UndefinedBehavior e
URemByZero (RegValue' sym (BVType w)
 -> RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO
     (RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
forall (w :: Natural).
(1 <= w) =>
RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
bv RegValue' sym (BVType w)
v1 IO (RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO (UndefinedBehavior (RegValue' sym))
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
forall (w :: Natural).
(1 <= w) =>
RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
bv RegValue' sym (BVType w)
v2
    SRemByZero RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ->
      RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> e (BVType w) -> UndefinedBehavior e
SRemByZero (RegValue' sym (BVType w)
 -> RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO
     (RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
forall (w :: Natural).
(1 <= w) =>
RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
bv RegValue' sym (BVType w)
v1 IO (RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO (UndefinedBehavior (RegValue' sym))
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
forall (w :: Natural).
(1 <= w) =>
RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
bv RegValue' sym (BVType w)
v2
    SDivOverflow RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ->
      RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> e (BVType w) -> UndefinedBehavior e
SDivOverflow (RegValue' sym (BVType w)
 -> RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO
     (RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
forall (w :: Natural).
(1 <= w) =>
RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
bv RegValue' sym (BVType w)
v1 IO (RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO (UndefinedBehavior (RegValue' sym))
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
forall (w :: Natural).
(1 <= w) =>
RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
bv RegValue' sym (BVType w)
v2
    SRemOverflow RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ->
      RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> e (BVType w) -> UndefinedBehavior e
SRemOverflow (RegValue' sym (BVType w)
 -> RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO
     (RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
forall (w :: Natural).
(1 <= w) =>
RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
bv RegValue' sym (BVType w)
v1 IO (RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO (UndefinedBehavior (RegValue' sym))
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
forall (w :: Natural).
(1 <= w) =>
RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
bv RegValue' sym (BVType w)
v2
    AbsIntMin RegValue' sym (BVType w)
v ->
      RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> UndefinedBehavior e
AbsIntMin (RegValue' sym (BVType w) -> UndefinedBehavior (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO (UndefinedBehavior (RegValue' sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
forall (w :: Natural).
(1 <= w) =>
RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
bv RegValue' sym (BVType w)
v

    PoisonValueCreated Poison (RegValue' sym)
poison ->
      Poison (RegValue' sym) -> UndefinedBehavior (RegValue' sym)
forall (e :: CrucibleType -> Type). Poison e -> UndefinedBehavior e
PoisonValueCreated (Poison (RegValue' sym) -> UndefinedBehavior (RegValue' sym))
-> IO (Poison (RegValue' sym))
-> IO (UndefinedBehavior (RegValue' sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> Poison (RegValue' sym)
-> IO (Poison (RegValue' sym))
forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> Poison (RegValue' sym)
-> IO (Poison (RegValue' sym))
Poison.concPoison sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc Poison (RegValue' sym)
poison