-- |
-- 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(..), 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
  -- | 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
  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

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

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


-- | 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.
  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


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

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