-- |
-- Module           : Lang.Crucible.LLVM.Errors.Poison
-- Description      : All about LLVM poison values
-- Copyright        : (c) Galois, Inc 2018
-- License          : BSD3
-- Maintainer       : Langston Barrett <lbarrett@galois.com>
-- Stability        : provisional
--
-- This module is intended to be imported qualified.
--
-- Undefined values follow control flow, wereas the poison values follow data
-- flow. See the module-level comment in "Lang.Crucible.LLVM.Translation".
--
-- This email provides an explanation and motivation for poison and @undef@
-- values: https://lists.llvm.org/pipermail/llvm-dev/2016-October/106182.html
--------------------------------------------------------------------------

{-# 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(..), OrdF(..), 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 qualified What4.InterpretedFloatingPoint as W4IFP
import           What4.Expr (ExprBuilder, Flags, FloatModeRepr(..), GroundValue)
import qualified What4.Expr.GroundEval as W4GE

data Poison (e :: CrucibleType -> Type) where
  -- | Arguments: @op1@, @op2@
  AddNoUnsignedWrap   :: (1 <= w) => e (BVType w)
                      -> e (BVType w)
                      -> Poison e
  -- | Arguments: @op1@, @op2@
  AddNoSignedWrap     :: (1 <= w) => e (BVType w)
                      -> e (BVType w)
                      -> Poison e
  -- | Arguments: @op1@, @op2@
  SubNoUnsignedWrap   :: (1 <= w) => e (BVType w)
                      -> e (BVType w)
                      -> Poison e
  -- | Arguments: @op1@, @op2@
  SubNoSignedWrap     :: (1 <= w) => e (BVType w)
                      -> e (BVType w)
                      -> Poison e
  -- | Arguments: @op1@, @op2@
  MulNoUnsignedWrap   :: (1 <= w) => e (BVType w)
                      -> e (BVType w)
                      -> Poison e
  -- | Arguments: @op1@, @op2@
  MulNoSignedWrap     :: (1 <= w) => e (BVType w)
                      -> e (BVType w)
                      -> Poison e
  -- | Arguments: @op1@, @op2@
  UDivExact           :: (1 <= w) => e (BVType w)
                      -> e (BVType w)
                      -> Poison e
  -- | Arguments: @op1@, @op2@
  SDivExact           :: (1 <= w) => e (BVType w)
                      -> e (BVType w)
                      -> Poison e
  -- | Arguments: @op1@, @op2@
  ShlOp2Big           :: (1 <= w) => e (BVType w)
                      -> e (BVType w)
                      -> Poison e
  -- | Arguments: @op1@, @op2@
  ShlNoUnsignedWrap   :: (1 <= w) => e (BVType w)
                      -> e (BVType w)
                      -> Poison e
  -- | Arguments: @op1@, @op2@
  ShlNoSignedWrap     :: (1 <= w) => e (BVType w)
                      -> e (BVType w)
                      -> Poison e
  -- | Arguments: @op1@, @op2@
  LshrExact           :: (1 <= w) => e (BVType w)
                      -> e (BVType w)
                      -> Poison e
  -- | Arguments: @op1@, @op2@
  LshrOp2Big          :: (1 <= w) => e (BVType w)
                      -> e (BVType w)
                      -> Poison e
  -- | Arguments: @op1@, @op2@
  AshrExact           :: (1 <= w) => e (BVType w)
                      -> e (BVType w)
                      -> Poison e
  -- | Arguments: @op1@, @op2@
  AshrOp2Big          :: (1 <= w) => e (BVType w)
                      -> e (BVType w)
                      -> Poison e
  -- | TODO(langston): store the 'Vector'
  ExtractElementIndex :: (1 <= w) => e (BVType w)
                      -> Poison e
  -- | TODO(langston): store the 'Vector'
  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
  ZExtNonNegative     :: (1 <= w)
                      => e (BVType w)
                      -> Poison e
  UiToFpNonNegative   :: (1 <= w)
                      => e (BVType w)
                      -> Poison e
  FpToUiNotRepresentable
                      :: (1 <= w)
                      => FloatInfoRepr fi
                      -> e (FloatType fi)
                      -> NatRepr w
                      -> Poison e
  FpToSiNotRepresentable
                      :: (1 <= w)
                      => FloatInfoRepr fi
                      -> e (FloatType fi)
                      -> NatRepr w
                      -> Poison e
  TruncNoUnsignedWrap :: (1 <= w)
                      => e (BVType w)
                      -> Poison e
  TruncNoSignedWrap   :: (1 <= w)
                      => e (BVType w)
                      -> Poison e
  ICmpSameSign        :: (1 <= w)
                      => e (BVType w)
                      -> 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
    ZExtNonNegative e (BVType w)
_       -> LLVMRefVer -> Standard
LLVMRef LLVMRefVer
LLVM18
    UiToFpNonNegative e (BVType w)
_     -> LLVMRefVer -> Standard
LLVMRef LLVMRefVer
LLVM19
    FpToUiNotRepresentable FloatInfoRepr fi
_ e (FloatType fi)
_ NatRepr w
_ -> LLVMRefVer -> Standard
LLVMRef LLVMRefVer
LLVM8
    FpToSiNotRepresentable FloatInfoRepr fi
_ e (FloatType fi)
_ NatRepr w
_ -> LLVMRefVer -> Standard
LLVMRef LLVMRefVer
LLVM8
    TruncNoUnsignedWrap e (BVType w)
_   -> LLVMRefVer -> Standard
LLVMRef LLVMRefVer
LLVM20
    TruncNoSignedWrap e (BVType w)
_     -> LLVMRefVer -> Standard
LLVMRef LLVMRefVer
LLVM20
    ICmpSameSign e (BVType w)
_ e (BVType w)
_        -> LLVMRefVer -> Standard
LLVMRef LLVMRefVer
LLVM20

-- | Which section(s) of the document state that this is poison?
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)"
    ZExtNonNegative e (BVType w)
_       -> Doc ann
"‘zext’ Instruction (Semantics)"
    UiToFpNonNegative e (BVType w)
_     -> Doc ann
"‘uitofp’ Instruction (Semantics)"
    FpToUiNotRepresentable FloatInfoRepr fi
_ e (FloatType fi)
_ NatRepr w
_ -> Doc ann
"‘fptoui’ Instruction (Semantics)"
    FpToSiNotRepresentable FloatInfoRepr fi
_ e (FloatType fi)
_ NatRepr w
_ -> Doc ann
"‘fptosi’ Instruction (Semantics)"
    TruncNoUnsignedWrap e (BVType w)
_   -> Doc ann
"‘trunc’ Instruction (Semantics)"
    TruncNoSignedWrap e (BVType w)
_     -> Doc ann
"‘trunc’ Instruction (Semantics)"
    ICmpSameSign e (BVType w)
_ e (BVType w)
_        -> Doc ann
"‘icmp’ 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`"
      ]

    -- The following explanation is a bit unsatisfactory, because it is specific
    -- to how we treat this instruction in Crucible. (See also #1605.)
    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` attribute set."
      ]

    ZExtNonNegative e (BVType w)
_ ->
      Doc ann
"A negative integer was zero-extended even though the `nneg` flag was set"
    UiToFpNonNegative e (BVType w)
_ ->
      Doc ann
"A negative integer was converted to a floating-point value even though the `nneg` flag was set"
    FpToUiNotRepresentable FloatInfoRepr fi
_ e (FloatType fi)
_ NatRepr 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
"A floating-point value was converted to an unsigned integer,"
      , Doc ann
"even though the value does not fit in the unsigned integer's type"
      ]
    FpToSiNotRepresentable FloatInfoRepr fi
_ e (FloatType fi)
_ NatRepr 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
"A floating-point value was converted to a signed integer,"
      , Doc ann
"even though the value does not fit in the signed integer's type"
      ]
    TruncNoUnsignedWrap e (BVType w)
_ ->
      Doc ann
"Unsigned truncation caused wrapping even though the `nuw` flag was set"
    TruncNoSignedWrap e (BVType w)
_ ->
      Doc ann
"Signed truncation caused wrapping even though the `nsw` flag was set"
    ICmpSameSign e (BVType w)
_ e (BVType w)
_ ->
      Doc ann
"Two integers with different signs were compared even though the `samesign` flag was 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
      ]
    ZExtNonNegative 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]
    UiToFpNonNegative 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]
    FpToUiNotRepresentable FloatInfoRepr fi
fi (RV RegValue sym (FloatType fi)
float) NatRepr w
bvW ->
      [ Doc ann
"Floating-point type:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> FloatInfoRepr fi -> Doc ann
forall ann. FloatInfoRepr fi -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty FloatInfoRepr fi
fi
      , Doc ann
"Floating-point value:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> SymExpr sym (SymInterpretedFloatType sym fi) -> 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 (FloatType fi)
SymExpr sym (SymInterpretedFloatType sym fi)
float
      , Doc ann
"Unsigned integer size (in bits):" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> NatRepr w -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow NatRepr w
bvW
      ]
    FpToSiNotRepresentable FloatInfoRepr fi
fi (RV RegValue sym (FloatType fi)
float) NatRepr w
bvW ->
      [ Doc ann
"Floating-point type:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> FloatInfoRepr fi -> Doc ann
forall ann. FloatInfoRepr fi -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty FloatInfoRepr fi
fi
      , Doc ann
"Floating-point value:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> SymExpr sym (SymInterpretedFloatType sym fi) -> 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 (FloatType fi)
SymExpr sym (SymInterpretedFloatType sym fi)
float
      , Doc ann
"Signed integer size (in bits):" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> NatRepr w -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow NatRepr w
bvW
      ]
    TruncNoUnsignedWrap 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]
    TruncNoSignedWrap 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]
    ICmpSameSign 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]

 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) ]


-- | Pretty print an error message relating to LLVM poison values,
--   when given a printer to produce a detailed message.
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  -> []

-- | Pretty print an error message relating to LLVM poison values
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

-- | Concretize a poison error message.
concPoison :: forall sym t st fm.
  ( W4I.IsExprBuilder sym
  , sym ~ ExprBuilder t st (Flags fm)
  ) =>
  sym ->
  FloatModeRepr fm ->
  (forall tp. W4I.SymExpr sym tp -> IO (GroundValue tp)) ->
  Poison (RegValue' sym) -> IO (Poison (RegValue' sym))
concPoison :: forall sym t (st :: Type -> Type) (fm :: FloatMode).
(IsExprBuilder sym, sym ~ ExprBuilder t st (Flags fm)) =>
sym
-> FloatModeRepr fm
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> Poison (RegValue' sym)
-> IO (Poison (RegValue' sym))
concPoison sym
sym FloatModeRepr fm
fm 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)
Expr t ('BaseBVType w) -> RegValue' sym (BVType w)
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
RV (Expr t ('BaseBVType w) -> RegValue' sym (BVType w))
-> IO (Expr t ('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))
-> SymBV sym w
-> IO (SymBV sym 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)
SymBV sym w
x

      fp ::
        forall fi.
        FloatInfoRepr fi ->
        RegValue' sym (FloatType fi) ->
        IO (RegValue' sym (FloatType fi))
      fp :: forall (fi :: FloatInfo).
FloatInfoRepr fi
-> RegValue' sym (FloatType fi)
-> IO (RegValue' sym (FloatType fi))
fp FloatInfoRepr fi
fi (RV RegValue sym (FloatType fi)
x) = do
        GroundValue
  (SymInterpretedFloatType (ExprBuilder t st (Flags fm)) fi)
v <- SymExpr
  sym (SymInterpretedFloatType (ExprBuilder t st (Flags fm)) fi)
-> IO
     (GroundValue
        (SymInterpretedFloatType (ExprBuilder t st (Flags fm)) fi))
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc RegValue sym (FloatType fi)
SymExpr
  sym (SymInterpretedFloatType (ExprBuilder t st (Flags fm)) fi)
x
        Expr t (SymInterpretedFloatType (ExprBuilder t st (Flags fm)) fi)
rv <-
          case FloatModeRepr fm
fm of
            FloatModeRepr fm
FloatIEEERepr ->
              sym
-> FloatPrecisionRepr (FloatInfoToPrecision fi)
-> BigFloat
-> IO (SymFloat sym (FloatInfoToPrecision fi))
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
forall (fpp :: FloatPrecision).
sym -> FloatPrecisionRepr fpp -> BigFloat -> IO (SymFloat sym fpp)
W4I.floatLit sym
sym (FloatInfoRepr fi -> FloatPrecisionRepr (FloatInfoToPrecision fi)
forall (fi :: FloatInfo).
FloatInfoRepr fi -> FloatPrecisionRepr (FloatInfoToPrecision fi)
floatInfoToPrecisionRepr FloatInfoRepr fi
fi) BigFloat
GroundValue
  (SymInterpretedFloatType (ExprBuilder t st (Flags fm)) fi)
v
            FloatModeRepr fm
FloatUninterpretedRepr -> do
              Expr t (BaseBVType (FloatInfoToBitWidth fi))
sv <- sym
-> BaseTypeRepr (BaseBVType (FloatInfoToBitWidth fi))
-> GroundValue (BaseBVType (FloatInfoToBitWidth fi))
-> IO (SymExpr sym (BaseBVType (FloatInfoToBitWidth fi)))
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> BaseTypeRepr tp -> GroundValue tp -> IO (SymExpr sym tp)
W4GE.groundToSym sym
sym (FloatInfoRepr fi
-> BaseTypeRepr (BaseBVType (FloatInfoToBitWidth fi))
forall (fi :: FloatInfo).
FloatInfoRepr fi
-> BaseTypeRepr (BaseBVType (FloatInfoToBitWidth fi))
floatInfoToBVTypeRepr FloatInfoRepr fi
fi) GroundValue
  (SymInterpretedFloatType (ExprBuilder t st (Flags fm)) fi)
GroundValue (BaseBVType (FloatInfoToBitWidth fi))
v
              sym
-> FloatInfoRepr fi
-> SymExpr sym (BaseBVType (FloatInfoToBitWidth fi))
-> IO (SymInterpretedFloat sym fi)
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi
-> SymBV sym (FloatInfoToBitWidth fi)
-> IO (SymInterpretedFloat sym fi)
forall (fi :: FloatInfo).
sym
-> FloatInfoRepr fi
-> SymBV sym (FloatInfoToBitWidth fi)
-> IO (SymInterpretedFloat sym fi)
W4IFP.iFloatFromBinary sym
sym FloatInfoRepr fi
fi Expr t (BaseBVType (FloatInfoToBitWidth fi))
SymExpr sym (BaseBVType (FloatInfoToBitWidth fi))
sv
            FloatModeRepr fm
FloatRealRepr ->
              sym
-> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat sym fi)
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat sym fi)
forall (fi :: FloatInfo).
sym
-> FloatInfoRepr fi -> Rational -> IO (SymInterpretedFloat sym fi)
W4IFP.iFloatLitRational sym
sym FloatInfoRepr fi
fi Rational
GroundValue
  (SymInterpretedFloatType (ExprBuilder t st (Flags fm)) fi)
v
        RegValue' sym (FloatType fi) -> IO (RegValue' sym (FloatType fi))
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (RegValue' sym (FloatType fi) -> IO (RegValue' sym (FloatType fi)))
-> RegValue' sym (FloatType fi)
-> IO (RegValue' sym (FloatType fi))
forall a b. (a -> b) -> a -> b
$ RegValue sym (FloatType fi) -> RegValue' sym (FloatType fi)
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
RV RegValue sym (FloatType fi)
Expr t (SymInterpretedFloatType (ExprBuilder t st (Flags fm)) fi)
rv 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) (fi :: Natural) (e :: CrucibleType -> Type).
(1 <= w, 1 <= fi) =>
e (LLVMPointerType fi) -> 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
    ZExtNonNegative 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
ZExtNonNegative (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
    UiToFpNonNegative 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
UiToFpNonNegative (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
    FpToUiNotRepresentable FloatInfoRepr fi
v1 RegValue' sym (FloatType fi)
v2 NatRepr w
v3 ->
      FloatInfoRepr fi
-> RegValue' sym (FloatType fi)
-> NatRepr w
-> Poison (RegValue' sym)
forall (w :: Natural) (fi :: FloatInfo)
       (e :: CrucibleType -> Type).
(1 <= w) =>
FloatInfoRepr fi -> e (FloatType fi) -> NatRepr w -> Poison e
FpToUiNotRepresentable FloatInfoRepr fi
v1 (RegValue' sym (FloatType fi)
 -> NatRepr w -> Poison (RegValue' sym))
-> IO (RegValue' sym (FloatType fi))
-> IO (NatRepr w -> Poison (RegValue' sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> FloatInfoRepr fi
-> RegValue' sym (FloatType fi)
-> IO (RegValue' sym (FloatType fi))
forall (fi :: FloatInfo).
FloatInfoRepr fi
-> RegValue' sym (FloatType fi)
-> IO (RegValue' sym (FloatType fi))
fp FloatInfoRepr fi
v1 RegValue' sym (FloatType fi)
v2 IO (NatRepr w -> Poison (RegValue' sym))
-> IO (NatRepr 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
<*> NatRepr w -> IO (NatRepr w)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure NatRepr w
v3
    FpToSiNotRepresentable FloatInfoRepr fi
v1 RegValue' sym (FloatType fi)
v2 NatRepr w
v3 ->
      FloatInfoRepr fi
-> RegValue' sym (FloatType fi)
-> NatRepr w
-> Poison (RegValue' sym)
forall (w :: Natural) (fi :: FloatInfo)
       (e :: CrucibleType -> Type).
(1 <= w) =>
FloatInfoRepr fi -> e (FloatType fi) -> NatRepr w -> Poison e
FpToSiNotRepresentable FloatInfoRepr fi
v1 (RegValue' sym (FloatType fi)
 -> NatRepr w -> Poison (RegValue' sym))
-> IO (RegValue' sym (FloatType fi))
-> IO (NatRepr w -> Poison (RegValue' sym))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> FloatInfoRepr fi
-> RegValue' sym (FloatType fi)
-> IO (RegValue' sym (FloatType fi))
forall (fi :: FloatInfo).
FloatInfoRepr fi
-> RegValue' sym (FloatType fi)
-> IO (RegValue' sym (FloatType fi))
fp FloatInfoRepr fi
v1 RegValue' sym (FloatType fi)
v2 IO (NatRepr w -> Poison (RegValue' sym))
-> IO (NatRepr 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
<*> NatRepr w -> IO (NatRepr w)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure NatRepr w
v3
    TruncNoUnsignedWrap 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
TruncNoUnsignedWrap (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
    TruncNoSignedWrap 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
TruncNoSignedWrap (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
    ICmpSameSign 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
ICmpSameSign (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


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

-- The weirdness in these instances is due to existential quantification over
-- the width. We have to make sure the type variable doesn't escape its scope.

$(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' |])
       , ( U.ConType [t| FloatInfoRepr |] `U.TypeApp` U.AnyType, [| testEquality |])
       , ( U.ConType [t| NatRepr |] `U.TypeApp` U.AnyType, [| testEquality |])
       ])

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' |])
       , ( U.ConType [t| FloatInfoRepr |] `U.TypeApp` U.AnyType, [| compareF |])
       , ( U.ConType [t| NatRepr |] `U.TypeApp` U.AnyType, [| compareF |])
       ])

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
         , [| ($) |] -- \f x -> f x
         )
       ]
     )