{-# 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
(
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)
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 (<=)"
data UndefinedBehavior (e :: CrucibleType -> Type) where
FreeBadOffset ::
(1 <= w) =>
e (LLVMPointerType w) ->
UndefinedBehavior e
FreeUnallocated ::
(1 <= w) =>
e (LLVMPointerType w) ->
UndefinedBehavior e
DoubleFree ::
(1 <= w) =>
e (LLVMPointerType w) ->
UndefinedBehavior e
MemsetInvalidRegion ::
(1 <= w, 1 <= v) =>
e (LLVMPointerType w) ->
e (BVType 8) ->
e (BVType v) ->
UndefinedBehavior e
ReadBadAlignment ::
(1 <= w) =>
e (LLVMPointerType w) ->
Alignment ->
UndefinedBehavior e
WriteBadAlignment ::
(1 <= w) =>
e (LLVMPointerType w) ->
Alignment ->
UndefinedBehavior e
PtrAddOffsetOutOfBounds ::
(1 <= w) =>
e (LLVMPointerType w) ->
e (BVType w) ->
UndefinedBehavior e
CompareInvalidPointer ::
(1 <= w) =>
PtrComparisonOperator ->
e (LLVMPointerType w) ->
e (LLVMPointerType w) ->
UndefinedBehavior e
CompareDifferentAllocs ::
(1 <= w) =>
e (LLVMPointerType w) ->
e (LLVMPointerType w) ->
UndefinedBehavior e
PtrSubDifferentAllocs ::
(1 <= w) =>
e (LLVMPointerType w) ->
e (LLVMPointerType w) ->
UndefinedBehavior e
PointerIntCast ::
(1 <= w) =>
e (LLVMPointerType w) ->
StorageType ->
UndefinedBehavior e
PointerUnsupportedOp ::
(1 <= w) =>
e (LLVMPointerType w) ->
String ->
UndefinedBehavior e
PointerFloatCast ::
(1 <= w) =>
e (LLVMPointerType w) ->
StorageType ->
UndefinedBehavior e
ComparePointerToBV ::
(1 <= w) =>
e (LLVMPointerType w) ->
e (BVType w) ->
UndefinedBehavior e
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
AbsIntMin :: (1 <= w) => e (BVType w) -> UndefinedBehavior e
PoisonValueCreated ::
Poison.Poison e ->
UndefinedBehavior e
deriving (Typeable)
standard :: UndefinedBehavior e -> Standard
standard :: forall (e :: CrucibleType -> Type). UndefinedBehavior e -> Standard
standard =
\case
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
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
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
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
cite :: UndefinedBehavior e -> Doc ann
cite :: forall (e :: CrucibleType -> Type) ann.
UndefinedBehavior e -> Doc ann
cite =
\case
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"
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"
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"
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
explain :: UndefinedBehavior e -> Doc ann
explain :: forall (e :: CrucibleType -> Type) ann.
UndefinedBehavior e -> Doc ann
explain =
\case
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"
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"
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)"
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 ]
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
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 ->
[ 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 ->
[ 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
]
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
]
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 ]
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])
-> 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)
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 -> [])
$(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