{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StrictData #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}
module Lang.Crucible.LLVM.Errors.Poison
( Poison(..)
, cite
, explain
, standard
, details
, pp
, ppReg
, concPoison
) where
import Data.Kind (Type)
import Data.Maybe (isJust)
import Data.Typeable (Typeable)
import Prettyprinter
import qualified Data.Parameterized.TraversableF as TF
import Data.Parameterized.TraversableF (FunctorF(..), FoldableF(..), TraversableF(..))
import qualified Data.Parameterized.TH.GADT as U
import Data.Parameterized.ClassesC (TestEqualityC(..), OrdC(..))
import Data.Parameterized.Classes (OrderingF(..), toOrdering)
import Lang.Crucible.LLVM.Errors.Standards
import Lang.Crucible.LLVM.MemModel.Pointer (LLVMPointerType, concBV, concPtr', ppPtr)
import Lang.Crucible.Simulator.RegValue (RegValue'(..))
import Lang.Crucible.Types
import qualified What4.Interface as W4I
import What4.Expr (GroundValue)
data Poison (e :: CrucibleType -> Type) where
AddNoUnsignedWrap :: (1 <= w) => e (BVType w)
-> e (BVType w)
-> Poison e
AddNoSignedWrap :: (1 <= w) => e (BVType w)
-> e (BVType w)
-> Poison e
SubNoUnsignedWrap :: (1 <= w) => e (BVType w)
-> e (BVType w)
-> Poison e
SubNoSignedWrap :: (1 <= w) => e (BVType w)
-> e (BVType w)
-> Poison e
MulNoUnsignedWrap :: (1 <= w) => e (BVType w)
-> e (BVType w)
-> Poison e
MulNoSignedWrap :: (1 <= w) => e (BVType w)
-> e (BVType w)
-> Poison e
UDivExact :: (1 <= w) => e (BVType w)
-> e (BVType w)
-> Poison e
SDivExact :: (1 <= w) => e (BVType w)
-> e (BVType w)
-> Poison e
ShlOp2Big :: (1 <= w) => e (BVType w)
-> e (BVType w)
-> Poison e
ShlNoUnsignedWrap :: (1 <= w) => e (BVType w)
-> e (BVType w)
-> Poison e
ShlNoSignedWrap :: (1 <= w) => e (BVType w)
-> e (BVType w)
-> Poison e
LshrExact :: (1 <= w) => e (BVType w)
-> e (BVType w)
-> Poison e
LshrOp2Big :: (1 <= w) => e (BVType w)
-> e (BVType w)
-> Poison e
AshrExact :: (1 <= w) => e (BVType w)
-> e (BVType w)
-> Poison e
AshrOp2Big :: (1 <= w) => e (BVType w)
-> e (BVType w)
-> Poison e
:: (1 <= w) => e (BVType w)
-> Poison e
InsertElementIndex :: (1 <= w) => e (BVType w)
-> Poison e
LLVMAbsIntMin :: (1 <= w) => e (BVType w)
-> Poison e
GEPOutOfBounds :: (1 <= w, 1 <= wptr) => e (LLVMPointerType wptr)
-> e (BVType w)
-> Poison e
deriving (Typeable)
standard :: Poison e -> Standard
standard :: forall (e :: CrucibleType -> Type). Poison e -> Standard
standard =
\case
AddNoUnsignedWrap e (BVType w)
_ e (BVType w)
_ -> LLVMRefVer -> Standard
LLVMRef LLVMRefVer
LLVM8
AddNoSignedWrap e (BVType w)
_ e (BVType w)
_ -> LLVMRefVer -> Standard
LLVMRef LLVMRefVer
LLVM8
SubNoUnsignedWrap e (BVType w)
_ e (BVType w)
_ -> LLVMRefVer -> Standard
LLVMRef LLVMRefVer
LLVM8
SubNoSignedWrap e (BVType w)
_ e (BVType w)
_ -> LLVMRefVer -> Standard
LLVMRef LLVMRefVer
LLVM8
MulNoUnsignedWrap e (BVType w)
_ e (BVType w)
_ -> LLVMRefVer -> Standard
LLVMRef LLVMRefVer
LLVM8
MulNoSignedWrap e (BVType w)
_ e (BVType w)
_ -> LLVMRefVer -> Standard
LLVMRef LLVMRefVer
LLVM8
UDivExact e (BVType w)
_ e (BVType w)
_ -> LLVMRefVer -> Standard
LLVMRef LLVMRefVer
LLVM8
SDivExact e (BVType w)
_ e (BVType w)
_ -> LLVMRefVer -> Standard
LLVMRef LLVMRefVer
LLVM8
ShlOp2Big e (BVType w)
_ e (BVType w)
_ -> LLVMRefVer -> Standard
LLVMRef LLVMRefVer
LLVM8
ShlNoUnsignedWrap e (BVType w)
_ e (BVType w)
_ -> LLVMRefVer -> Standard
LLVMRef LLVMRefVer
LLVM8
ShlNoSignedWrap e (BVType w)
_ e (BVType w)
_ -> LLVMRefVer -> Standard
LLVMRef LLVMRefVer
LLVM8
LshrExact e (BVType w)
_ e (BVType w)
_ -> LLVMRefVer -> Standard
LLVMRef LLVMRefVer
LLVM8
LshrOp2Big e (BVType w)
_ e (BVType w)
_ -> LLVMRefVer -> Standard
LLVMRef LLVMRefVer
LLVM8
AshrExact e (BVType w)
_ e (BVType w)
_ -> LLVMRefVer -> Standard
LLVMRef LLVMRefVer
LLVM8
AshrOp2Big e (BVType w)
_ e (BVType w)
_ -> LLVMRefVer -> Standard
LLVMRef LLVMRefVer
LLVM8
ExtractElementIndex e (BVType w)
_ -> LLVMRefVer -> Standard
LLVMRef LLVMRefVer
LLVM8
InsertElementIndex e (BVType w)
_ -> LLVMRefVer -> Standard
LLVMRef LLVMRefVer
LLVM8
LLVMAbsIntMin e (BVType w)
_ -> LLVMRefVer -> Standard
LLVMRef LLVMRefVer
LLVM12
GEPOutOfBounds e (LLVMPointerType wptr)
_ e (BVType w)
_ -> LLVMRefVer -> Standard
LLVMRef LLVMRefVer
LLVM8
cite :: Poison e -> Doc ann
cite :: forall (e :: CrucibleType -> Type) ann. Poison e -> Doc ann
cite =
\case
AddNoUnsignedWrap e (BVType w)
_ e (BVType w)
_ -> Doc ann
"‘add’ Instruction (Semantics)"
AddNoSignedWrap e (BVType w)
_ e (BVType w)
_ -> Doc ann
"‘add’ Instruction (Semantics)"
SubNoUnsignedWrap e (BVType w)
_ e (BVType w)
_ -> Doc ann
"‘sub’ Instruction (Semantics)"
SubNoSignedWrap e (BVType w)
_ e (BVType w)
_ -> Doc ann
"‘sub’ Instruction (Semantics)"
MulNoUnsignedWrap e (BVType w)
_ e (BVType w)
_ -> Doc ann
"‘mul’ Instruction (Semantics)"
MulNoSignedWrap e (BVType w)
_ e (BVType w)
_ -> Doc ann
"‘mul’ Instruction (Semantics)"
UDivExact e (BVType w)
_ e (BVType w)
_ -> Doc ann
"‘udiv’ Instruction (Semantics)"
SDivExact e (BVType w)
_ e (BVType w)
_ -> Doc ann
"‘sdiv’ Instruction (Semantics)"
ShlOp2Big e (BVType w)
_ e (BVType w)
_ -> Doc ann
"‘shl’ Instruction (Semantics)"
ShlNoUnsignedWrap e (BVType w)
_ e (BVType w)
_ -> Doc ann
"‘shl’ Instruction (Semantics)"
ShlNoSignedWrap e (BVType w)
_ e (BVType w)
_ -> Doc ann
"‘shl’ Instruction (Semantics)"
LshrExact e (BVType w)
_ e (BVType w)
_ -> Doc ann
"‘lshr’ Instruction (Semantics)"
LshrOp2Big e (BVType w)
_ e (BVType w)
_ -> Doc ann
"‘lshr’ Instruction (Semantics)"
AshrExact e (BVType w)
_ e (BVType w)
_ -> Doc ann
"‘ashr’ Instruction (Semantics)"
AshrOp2Big e (BVType w)
_ e (BVType w)
_ -> Doc ann
"‘ashr’ Instruction (Semantics)"
ExtractElementIndex e (BVType w)
_ -> Doc ann
"‘extractelement’ Instruction (Semantics)"
InsertElementIndex e (BVType w)
_ -> Doc ann
"‘insertelement’ Instruction (Semantics)"
LLVMAbsIntMin e (BVType w)
_ -> Doc ann
"‘llvm.abs.*’ Intrinsic (Semantics)"
GEPOutOfBounds e (LLVMPointerType wptr)
_ e (BVType w)
_ -> Doc ann
"‘getelementptr’ Instruction (Semantics)"
explain :: Poison e -> Doc ann
explain :: forall (e :: CrucibleType -> Type) ann. Poison e -> Doc ann
explain =
\case
AddNoUnsignedWrap e (BVType w)
_ e (BVType w)
_ ->
Doc ann
"Unsigned addition caused wrapping even though the `nuw` flag was set"
AddNoSignedWrap e (BVType w)
_ e (BVType w)
_ ->
Doc ann
"Signed addition caused wrapping even though the `nsw` flag was set"
SubNoUnsignedWrap e (BVType w)
_ e (BVType w)
_ ->
Doc ann
"Unsigned subtraction caused wrapping even though the `nuw` flag was set"
SubNoSignedWrap e (BVType w)
_ e (BVType w)
_ ->
Doc ann
"Signed subtraction caused wrapping even though the `nsw` flag was set"
MulNoUnsignedWrap e (BVType w)
_ e (BVType w)
_ ->
Doc ann
"Unsigned multiplication caused wrapping even though the `nuw` flag was set"
MulNoSignedWrap e (BVType w)
_ e (BVType w)
_ ->
Doc ann
"Signed multiplication caused wrapping even though the `nsw` flag was set"
SDivExact e (BVType w)
_ e (BVType w)
_ ->
Doc ann
"Inexact signed division even though the `exact` flag was set"
UDivExact e (BVType w)
_ e (BVType w)
_ ->
Doc ann
"Inexact unsigned division even though the `exact` flag was set"
ShlOp2Big e (BVType w)
_ e (BVType w)
_ ->
Doc ann
"The second operand of `shl` was equal to or greater than the number of bits in the first operand"
ShlNoUnsignedWrap e (BVType w)
_ e (BVType w)
_ ->
Doc ann
"Left shift shifted out non-zero bits even though the `nuw` flag was set"
ShlNoSignedWrap e (BVType w)
_ e (BVType w)
_ ->
Doc ann
"Left shift shifted out some bits that disagreed with the sign bit even though the `nsw` flag was set"
LshrExact e (BVType w)
_ e (BVType w)
_ ->
Doc ann
"Inexact `lshr` (logical right shift) result even though the `exact` flag was set"
LshrOp2Big e (BVType w)
_ e (BVType w)
_ ->
Doc ann
"The second operand of `lshr` was equal to or greater than the number of bits in the first operand"
AshrExact e (BVType w)
_ e (BVType w)
_ ->
Doc ann
"Inexact `ashr` (arithmetic right shift) result even though the `exact` flag was set"
AshrOp2Big e (BVType w)
_ e (BVType w)
_ ->
Doc ann
"The second operand of `ashr` was equal to or greater than the number of bits in the first operand"
ExtractElementIndex e (BVType 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
"Attempted to extract an element from a vector at an index that was"
, Doc ann
"greater than the length of the vector"
]
InsertElementIndex e (BVType 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
"Attempted to insert an element into a vector at an index that was"
, Doc ann
"greater than the length of the vector"
]
LLVMAbsIntMin e (BVType 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
"The first argument of `llvm.abs.*` was `INT_MIN` even though the"
, Doc ann
"second argument was `1`"
]
GEPOutOfBounds e (LLVMPointerType wptr)
_ e (BVType 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
"Calling `getelementptr` resulted in an index that was out of bounds for the"
, Doc ann
"given allocation (likely due to arithmetic overflow), but Crucible currently"
, Doc ann
"treats all GEP instructions as if they had the `inbounds` flag set."
]
details :: forall sym ann.
W4I.IsExpr (W4I.SymExpr sym) => Poison (RegValue' sym) -> [Doc ann]
details :: forall sym ann.
IsExpr (SymExpr sym) =>
Poison (RegValue' sym) -> [Doc ann]
details =
\case
AddNoUnsignedWrap RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 -> [RegValue' sym (BVType w)] -> [Doc ann]
forall (w :: Natural). [RegValue' sym (BVType w)] -> [Doc ann]
args [RegValue' sym (BVType w)
v1, RegValue' sym (BVType w)
v2]
AddNoSignedWrap RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 -> [RegValue' sym (BVType w)] -> [Doc ann]
forall (w :: Natural). [RegValue' sym (BVType w)] -> [Doc ann]
args [RegValue' sym (BVType w)
v1, RegValue' sym (BVType w)
v2]
SubNoUnsignedWrap RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 -> [RegValue' sym (BVType w)] -> [Doc ann]
forall (w :: Natural). [RegValue' sym (BVType w)] -> [Doc ann]
args [RegValue' sym (BVType w)
v1, RegValue' sym (BVType w)
v2]
SubNoSignedWrap RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 -> [RegValue' sym (BVType w)] -> [Doc ann]
forall (w :: Natural). [RegValue' sym (BVType w)] -> [Doc ann]
args [RegValue' sym (BVType w)
v1, RegValue' sym (BVType w)
v2]
MulNoUnsignedWrap RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 -> [RegValue' sym (BVType w)] -> [Doc ann]
forall (w :: Natural). [RegValue' sym (BVType w)] -> [Doc ann]
args [RegValue' sym (BVType w)
v1, RegValue' sym (BVType w)
v2]
MulNoSignedWrap RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 -> [RegValue' sym (BVType w)] -> [Doc ann]
forall (w :: Natural). [RegValue' sym (BVType w)] -> [Doc ann]
args [RegValue' sym (BVType w)
v1, RegValue' sym (BVType w)
v2]
SDivExact RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 -> [RegValue' sym (BVType w)] -> [Doc ann]
forall (w :: Natural). [RegValue' sym (BVType w)] -> [Doc ann]
args [RegValue' sym (BVType w)
v1, RegValue' sym (BVType w)
v2]
UDivExact RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 -> [RegValue' sym (BVType w)] -> [Doc ann]
forall (w :: Natural). [RegValue' sym (BVType w)] -> [Doc ann]
args [RegValue' sym (BVType w)
v1, RegValue' sym (BVType w)
v2]
ShlOp2Big RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 -> [RegValue' sym (BVType w)] -> [Doc ann]
forall (w :: Natural). [RegValue' sym (BVType w)] -> [Doc ann]
args [RegValue' sym (BVType w)
v1, RegValue' sym (BVType w)
v2]
ShlNoUnsignedWrap RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 -> [RegValue' sym (BVType w)] -> [Doc ann]
forall (w :: Natural). [RegValue' sym (BVType w)] -> [Doc ann]
args [RegValue' sym (BVType w)
v1, RegValue' sym (BVType w)
v2]
ShlNoSignedWrap RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 -> [RegValue' sym (BVType w)] -> [Doc ann]
forall (w :: Natural). [RegValue' sym (BVType w)] -> [Doc ann]
args [RegValue' sym (BVType w)
v1, RegValue' sym (BVType w)
v2]
LshrExact RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 -> [RegValue' sym (BVType w)] -> [Doc ann]
forall (w :: Natural). [RegValue' sym (BVType w)] -> [Doc ann]
args [RegValue' sym (BVType w)
v1, RegValue' sym (BVType w)
v2]
LshrOp2Big RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 -> [RegValue' sym (BVType w)] -> [Doc ann]
forall (w :: Natural). [RegValue' sym (BVType w)] -> [Doc ann]
args [RegValue' sym (BVType w)
v1, RegValue' sym (BVType w)
v2]
AshrExact RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 -> [RegValue' sym (BVType w)] -> [Doc ann]
forall (w :: Natural). [RegValue' sym (BVType w)] -> [Doc ann]
args [RegValue' sym (BVType w)
v1, RegValue' sym (BVType w)
v2]
AshrOp2Big RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 -> [RegValue' sym (BVType w)] -> [Doc ann]
forall (w :: Natural). [RegValue' sym (BVType w)] -> [Doc ann]
args [RegValue' sym (BVType w)
v1, RegValue' sym (BVType w)
v2]
ExtractElementIndex RegValue' sym (BVType w)
v -> [RegValue' sym (BVType w)] -> [Doc ann]
forall (w :: Natural). [RegValue' sym (BVType w)] -> [Doc ann]
args [RegValue' sym (BVType w)
v]
InsertElementIndex RegValue' sym (BVType w)
v -> [RegValue' sym (BVType w)] -> [Doc ann]
forall (w :: Natural). [RegValue' sym (BVType w)] -> [Doc ann]
args [RegValue' sym (BVType w)
v]
LLVMAbsIntMin RegValue' sym (BVType w)
v -> [RegValue' sym (BVType w)] -> [Doc ann]
forall (w :: Natural). [RegValue' sym (BVType w)] -> [Doc ann]
args [RegValue' sym (BVType w)
v]
GEPOutOfBounds (RV RegValue sym (LLVMPointerType wptr)
ptr) (RV RegValue sym (BVType w)
bv) ->
[ Doc ann
"Pointer:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> RegValue sym (LLVMPointerType wptr) -> Doc ann
forall sym (wptr :: Natural) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
ppPtr RegValue sym (LLVMPointerType wptr)
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 RegValue sym (BVType w)
SymExpr sym ('BaseBVType w)
bv
]
where
args :: forall w. [RegValue' sym (BVType w)] -> [Doc ann]
args :: forall (w :: Natural). [RegValue' sym (BVType w)] -> [Doc ann]
args [] = [ Doc ann
"No arguments" ]
args [RV RegValue sym (BVType w)
v] = [ Doc ann
"Argument:" 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)
v ]
args [RegValue' sym (BVType w)]
vs = [ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep (Doc ann
"Arguments:" Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: (RegValue' sym (BVType w) -> Doc ann)
-> [RegValue' sym (BVType w)] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (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)
-> (RegValue' sym (BVType w) -> SymExpr sym ('BaseBVType w))
-> RegValue' sym (BVType w)
-> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RegValue' sym (BVType w) -> RegValue sym (BVType w)
RegValue' sym (BVType w) -> SymExpr sym ('BaseBVType w)
forall sym (tp :: CrucibleType).
RegValue' sym tp -> RegValue sym tp
unRV) [RegValue' sym (BVType w)]
vs) ]
pp :: (Poison e -> [Doc ann]) -> Poison e -> Doc ann
pp :: forall (e :: CrucibleType -> Type) ann.
(Poison e -> [Doc ann]) -> Poison e -> Doc ann
pp Poison e -> [Doc ann]
extra Poison e
poison = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$
[ Doc ann
"Poison value encountered: "
, Poison e -> Doc ann
forall (e :: CrucibleType -> Type) ann. Poison e -> Doc ann
explain Poison e
poison
, [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat (Poison e -> [Doc ann]
extra Poison e
poison)
, [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
cat [ Doc ann
"Reference: "
, Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Standard -> Text
ppStd (Poison e -> Standard
forall (e :: CrucibleType -> Type). Poison e -> Standard
standard Poison e
poison))
, Poison e -> Doc ann
forall (e :: CrucibleType -> Type) ann. Poison e -> Doc ann
cite Poison e
poison
]
] [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ case Standard -> Maybe Text
stdURL (Poison e -> Standard
forall (e :: CrucibleType -> Type). Poison e -> Standard
standard Poison e
poison) of
Just Text
url -> [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 -> []
ppReg ::W4I.IsExpr (W4I.SymExpr sym) => Poison (RegValue' sym) -> Doc ann
ppReg :: forall sym ann.
IsExpr (SymExpr sym) =>
Poison (RegValue' sym) -> Doc ann
ppReg = (Poison (RegValue' sym) -> [Doc ann])
-> Poison (RegValue' sym) -> Doc ann
forall (e :: CrucibleType -> Type) ann.
(Poison e -> [Doc ann]) -> Poison e -> Doc ann
pp Poison (RegValue' sym) -> [Doc ann]
forall sym ann.
IsExpr (SymExpr sym) =>
Poison (RegValue' sym) -> [Doc ann]
details
concPoison :: forall sym.
W4I.IsExprBuilder sym =>
sym ->
(forall tp. W4I.SymExpr sym tp -> IO (GroundValue tp)) ->
Poison (RegValue' sym) -> IO (Poison (RegValue' sym))
concPoison :: forall sym.
IsExprBuilder sym =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> Poison (RegValue' sym)
-> IO (Poison (RegValue' sym))
concPoison sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc Poison (RegValue' sym)
poison =
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 Poison (RegValue' sym)
poison of
AddNoUnsignedWrap RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ->
RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> e (BVType w) -> Poison e
AddNoUnsignedWrap (RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO (RegValue' sym (BVType w) -> Poison (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) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w)) -> IO (Poison (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
AddNoSignedWrap RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ->
RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> e (BVType w) -> Poison e
AddNoSignedWrap (RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO (RegValue' sym (BVType w) -> Poison (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) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w)) -> IO (Poison (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
SubNoUnsignedWrap RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ->
RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> e (BVType w) -> Poison e
SubNoUnsignedWrap (RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO (RegValue' sym (BVType w) -> Poison (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) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w)) -> IO (Poison (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
SubNoSignedWrap RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ->
RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> e (BVType w) -> Poison e
SubNoSignedWrap (RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO (RegValue' sym (BVType w) -> Poison (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) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w)) -> IO (Poison (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
MulNoUnsignedWrap RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ->
RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> e (BVType w) -> Poison e
MulNoUnsignedWrap(RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO (RegValue' sym (BVType w) -> Poison (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) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w)) -> IO (Poison (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
MulNoSignedWrap RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ->
RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> e (BVType w) -> Poison e
MulNoSignedWrap (RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO (RegValue' sym (BVType w) -> Poison (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) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w)) -> IO (Poison (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
UDivExact RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ->
RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> e (BVType w) -> Poison e
UDivExact (RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO (RegValue' sym (BVType w) -> Poison (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) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w)) -> IO (Poison (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
SDivExact RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ->
RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> e (BVType w) -> Poison e
SDivExact (RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO (RegValue' sym (BVType w) -> Poison (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) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w)) -> IO (Poison (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
ShlOp2Big RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ->
RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> e (BVType w) -> Poison e
ShlOp2Big (RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO (RegValue' sym (BVType w) -> Poison (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) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w)) -> IO (Poison (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
ShlNoUnsignedWrap RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ->
RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> e (BVType w) -> Poison e
ShlNoUnsignedWrap (RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO (RegValue' sym (BVType w) -> Poison (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) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w)) -> IO (Poison (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
ShlNoSignedWrap RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ->
RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> e (BVType w) -> Poison e
ShlNoSignedWrap (RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO (RegValue' sym (BVType w) -> Poison (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) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w)) -> IO (Poison (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
LshrExact RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ->
RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> e (BVType w) -> Poison e
LshrExact (RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO (RegValue' sym (BVType w) -> Poison (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) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w)) -> IO (Poison (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
LshrOp2Big RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ->
RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> e (BVType w) -> Poison e
LshrOp2Big (RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO (RegValue' sym (BVType w) -> Poison (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) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w)) -> IO (Poison (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
AshrExact RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ->
RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> e (BVType w) -> Poison e
AshrExact (RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO (RegValue' sym (BVType w) -> Poison (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) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w)) -> IO (Poison (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
AshrOp2Big RegValue' sym (BVType w)
v1 RegValue' sym (BVType w)
v2 ->
RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> e (BVType w) -> Poison e
AshrOp2Big (RegValue' sym (BVType w)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w))
-> IO (RegValue' sym (BVType w) -> Poison (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) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w)) -> IO (Poison (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
ExtractElementIndex RegValue' sym (BVType w)
v ->
RegValue' sym (BVType w) -> Poison (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> Poison e
ExtractElementIndex (RegValue' sym (BVType w) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w)) -> IO (Poison (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
InsertElementIndex RegValue' sym (BVType w)
v ->
RegValue' sym (BVType w) -> Poison (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> Poison e
InsertElementIndex (RegValue' sym (BVType w) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w)) -> IO (Poison (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
GEPOutOfBounds RegValue' sym (LLVMPointerType wptr)
p RegValue' sym (BVType w)
v ->
RegValue' sym (LLVMPointerType wptr)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym)
forall (w :: Natural) (wptr :: Natural)
(e :: CrucibleType -> Type).
(1 <= w, 1 <= wptr) =>
e (LLVMPointerType wptr) -> e (BVType w) -> Poison e
GEPOutOfBounds (RegValue' sym (LLVMPointerType wptr)
-> RegValue' sym (BVType w) -> Poison (RegValue' sym))
-> IO (RegValue' sym (LLVMPointerType wptr))
-> IO (RegValue' sym (BVType w) -> Poison (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 wptr)
-> IO (RegValue' sym (LLVMPointerType wptr))
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 wptr)
p IO (RegValue' sym (BVType w) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w)) -> IO (Poison (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)
v
LLVMAbsIntMin RegValue' sym (BVType w)
v ->
RegValue' sym (BVType w) -> Poison (RegValue' sym)
forall (w :: Natural) (e :: CrucibleType -> Type).
(1 <= w) =>
e (BVType w) -> Poison e
LLVMAbsIntMin (RegValue' sym (BVType w) -> Poison (RegValue' sym))
-> IO (RegValue' sym (BVType w)) -> IO (Poison (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
$(return [])
eqcPoison :: forall e.
(forall t1 t2. e t1 -> e t2 -> Maybe (t1 :~: t2)) ->
Poison e -> Poison e -> Maybe (() :~: ())
eqcPoison :: forall (e :: CrucibleType -> Type).
(forall (t1 :: CrucibleType) (t2 :: CrucibleType).
e t1 -> e t2 -> Maybe (t1 :~: t2))
-> Poison e -> Poison e -> Maybe (() :~: ())
eqcPoison forall (t1 :: CrucibleType) (t2 :: CrucibleType).
e t1 -> e t2 -> Maybe (t1 :~: t2)
subterms =
let subterms' :: forall p q. e p -> e q -> Maybe (() :~: ())
subterms' :: forall (p :: CrucibleType) (q :: CrucibleType).
e p -> e q -> Maybe (() :~: ())
subterms' e p
a e q
b =
case e p -> e q -> Maybe (p :~: q)
forall (t1 :: CrucibleType) (t2 :: CrucibleType).
e t1 -> e t2 -> Maybe (t1 :~: t2)
subterms e p
a e q
b of
Just p :~: q
Refl -> (() :~: ()) -> Maybe (() :~: ())
forall a. a -> Maybe a
Just () :~: ()
forall {k} (a :: k). a :~: a
Refl
Maybe (p :~: q)
Nothing -> Maybe (() :~: ())
forall a. Maybe a
Nothing
in $(U.structuralTypeEquality [t|Poison|]
[ ( U.DataArg 0 `U.TypeApp` U.AnyType, [| subterms' |])
])
ordcPoison :: forall e f.
(forall t1 t2. e t1 -> f t2 -> OrderingF t1 t2) ->
Poison e -> Poison f -> OrderingF () ()
ordcPoison :: forall (e :: CrucibleType -> Type) (f :: CrucibleType -> Type).
(forall (t1 :: CrucibleType) (t2 :: CrucibleType).
e t1 -> f t2 -> OrderingF t1 t2)
-> Poison e -> Poison f -> OrderingF () ()
ordcPoison forall (t1 :: CrucibleType) (t2 :: CrucibleType).
e t1 -> f t2 -> OrderingF t1 t2
subterms =
let subterms' :: forall p q. e p -> f q -> OrderingF () ()
subterms' :: forall (p :: CrucibleType) (q :: CrucibleType).
e p -> f q -> OrderingF () ()
subterms' e p
a f q
b =
case e p -> f q -> OrderingF p q
forall (t1 :: CrucibleType) (t2 :: CrucibleType).
e t1 -> f t2 -> OrderingF t1 t2
subterms e p
a f q
b of
OrderingF p q
EQF -> (OrderingF () ()
forall {k} (x :: k). OrderingF x x
EQF :: OrderingF () ())
OrderingF p q
GTF -> (OrderingF () ()
forall {k} (x :: k) (y :: k). OrderingF x y
GTF :: OrderingF () ())
OrderingF p q
LTF -> (OrderingF () ()
forall {k} (x :: k) (y :: k). OrderingF x y
LTF :: OrderingF () ())
in $(U.structuralTypeOrd [t|Poison|]
[ ( U.DataArg 0 `U.TypeApp` U.AnyType, [| subterms' |])
])
instance TestEqualityC Poison where
testEqualityC :: forall (f :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> Maybe (x :~: y))
-> Poison f -> Poison f -> Bool
testEqualityC forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> Maybe (x :~: y)
subterms Poison f
x Poison f
y = Maybe (() :~: ()) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (() :~: ()) -> Bool) -> Maybe (() :~: ()) -> Bool
forall a b. (a -> b) -> a -> b
$ (forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> Maybe (x :~: y))
-> Poison f -> Poison f -> Maybe (() :~: ())
forall (e :: CrucibleType -> Type).
(forall (t1 :: CrucibleType) (t2 :: CrucibleType).
e t1 -> e t2 -> Maybe (t1 :~: t2))
-> Poison e -> Poison e -> Maybe (() :~: ())
eqcPoison f t1 -> f t2 -> Maybe (t1 :~: t2)
forall (x :: CrucibleType) (y :: CrucibleType).
f x -> f y -> Maybe (x :~: y)
subterms Poison f
x Poison f
y
instance OrdC Poison where
compareC :: forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType) (y :: CrucibleType).
f x -> g y -> OrderingF x y)
-> Poison f -> Poison g -> Ordering
compareC forall (x :: CrucibleType) (y :: CrucibleType).
f x -> g y -> OrderingF x y
subterms Poison f
x Poison g
y = OrderingF () () -> Ordering
forall {k} (x :: k) (y :: k). OrderingF x y -> Ordering
toOrdering (OrderingF () () -> Ordering) -> OrderingF () () -> Ordering
forall a b. (a -> b) -> a -> b
$ (forall (x :: CrucibleType) (y :: CrucibleType).
f x -> g y -> OrderingF x y)
-> Poison f -> Poison g -> OrderingF () ()
forall (e :: CrucibleType -> Type) (f :: CrucibleType -> Type).
(forall (t1 :: CrucibleType) (t2 :: CrucibleType).
e t1 -> f t2 -> OrderingF t1 t2)
-> Poison e -> Poison f -> OrderingF () ()
ordcPoison f t1 -> g t2 -> OrderingF t1 t2
forall (x :: CrucibleType) (y :: CrucibleType).
f x -> g y -> OrderingF x y
subterms Poison f
x Poison g
y
instance FunctorF Poison where
fmapF :: forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
(forall (x :: CrucibleType). f x -> g x) -> Poison f -> Poison g
fmapF = (forall (s :: CrucibleType). f s -> g s) -> Poison f -> Poison 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 Poison where
foldMapF :: forall m (e :: CrucibleType -> Type).
Monoid m =>
(forall (s :: CrucibleType). e s -> m) -> Poison e -> m
foldMapF = (forall (s :: CrucibleType). e s -> m) -> Poison 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 Poison where
traverseF :: forall m e f. Applicative m
=> (forall s. e s -> m (f s))
-> Poison e
-> m (Poison f)
traverseF :: forall (m :: Type -> Type) (e :: CrucibleType -> Type)
(f :: CrucibleType -> Type).
Applicative m =>
(forall (s :: CrucibleType). e s -> m (f s))
-> Poison e -> m (Poison f)
traverseF =
$(U.structuralTraversal [t|Poison|]
[ ( U.DataArg 0 `U.TypeApp` U.AnyType
, [| ($) |]
)
]
)