content: -- |
  -- Module           : Lang.Crucible.LLVM.Errors.UndefinedBehavior
  -- Description      : All about undefined behavior
  -- Copyright        : (c) Galois, Inc 2018
  -- License          : BSD3
  -- Maintainer       : Langston Barrett <lbarrett@galois.com>
  -- Stability        : provisional
  --
  -- This module is intended to be imported qualified.
  --
  -- This module serves as an ad-hoc reference for the sort of undefined behaviors
  -- that the Crucible LLVM memory model is aware of. The information contained
  -- here is used in
  --  * providing helpful error messages
  --  * configuring which safety checks to perform
  --
  -- Disabling checks for undefined behavior does not change the behavior of any
  -- memory operations. If it is used to enable the simulation of undefined
  -- behavior, the result is that any guarantees that Crucible provides about the
  -- code essentially have an additional hypothesis: that the LLVM
  -- compiler/hardware platform behave identically to Crucible's simulator when
  -- encountering such behavior.
  --
  -- See @crucible-llvm-cli/test-data/ub@ for tests demonstrating some of these.
  --------------------------------------------------------------------------
  
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE DeriveDataTypeable #-}
  {-# LANGUAGE DeriveGeneric #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE InstanceSigs #-}
  {-# LANGUAGE LambdaCase #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE PatternGuards #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE StrictData #-}
  {-# LANGUAGE TemplateHaskell #-}
  {-# LANGUAGE TypeOperators #-}
  
  module Lang.Crucible.LLVM.Errors.UndefinedBehavior
    (
    -- ** Undefined Behavior
      PtrComparisonOperator(..)
    , UndefinedBehavior(..)
    , cite
    , details
    , explain
    , ppDetails
    , ppCitation
    , pp
  
    , concUB
    ) where
  
  import           Prelude
  
  import           GHC.Generics (Generic)
  import           Data.Data (Data)
  import           Data.Kind (Type)
  import           Data.Maybe (isJust)
  import           Data.Typeable (Typeable)
  import           Prettyprinter
  
  import           Data.Parameterized.Classes (toOrdering, fromOrdering)
  import           Data.Parameterized.ClassesC (TestEqualityC(..), OrdC(..))
  import qualified Data.Parameterized.TH.GADT as U
  import           Data.Parameterized.TraversableF (FunctorF(..), FoldableF(..), TraversableF(..))
  import qualified Data.Parameterized.TraversableF as TF
  
  import qualified What4.Interface as W4I
  import           What4.Expr (GroundValue)
  
  import           Lang.Crucible.Types
  import           Lang.Crucible.Simulator.RegValue (RegValue'(..))
  import           Lang.Crucible.LLVM.DataLayout (Alignment, fromAlignment)
  import           Lang.Crucible.LLVM.Errors.Standards
  import qualified Lang.Crucible.LLVM.Errors.Poison as Poison
  import           Lang.Crucible.LLVM.MemModel.Pointer (ppPtr, concBV, concPtr')
  import           Lang.Crucible.LLVM.MemModel.Type (StorageType)
  import           Lang.Crucible.LLVM.Types (LLVMPointerType)
  
  -- -----------------------------------------------------------------------
  -- ** UndefinedBehavior
  
  -- | The various comparison operators you can use on pointers
  data PtrComparisonOperator =
      Eq
    | Leq
    deriving (Data, Eq, Generic, Enum, Ord, Read, Show)
  
  ppPtrComparison :: PtrComparisonOperator -> Doc ann
  ppPtrComparison Eq  = "Equality comparison (==)"
  ppPtrComparison Leq = "Ordering comparison (<=)"
  
  -- | This type is parameterized on a higher-kinded term constructor so that it
  -- can be instantiated for expressions at translation time (i.e. the 'Expr' in
  -- 'LLVMGenerator'), or for expressions at runtime ('SymExpr').
  --
  -- See 'cite' and 'explain' for what each constructor means at the C/LLVM level.
  --
  -- The commented-out constructors correspond to behaviors that don't have
  -- explicit checks yet (but probably should!).
  data UndefinedBehavior (e :: CrucibleType -> Type) where
  
    -- -------------------------------- Memory management
  
    FreeBadOffset ::
      (1 <= w) =>
      e (LLVMPointerType w) ->
      UndefinedBehavior e
  
    FreeUnallocated ::
      (1 <= w) =>
      e (LLVMPointerType w) ->
      UndefinedBehavior e
  
    DoubleFree ::
      (1 <= w) =>
      e (LLVMPointerType w) ->
      UndefinedBehavior e
  
    -- | Arguments: Destination pointer, fill byte, length
    MemsetInvalidRegion ::
      (1 <= w, 1 <= v) =>
      e (LLVMPointerType w) ->
      e (BVType 8) ->
      e (BVType v) ->
      UndefinedBehavior e
  
    -- | Arguments: Read destination, alignment
    ReadBadAlignment ::
      (1 <= w) =>
      e (LLVMPointerType w) ->
      Alignment ->
      UndefinedBehavior e
  
    -- | Arguments: Write destination, alignment
    WriteBadAlignment ::
      (1 <= w) =>
      e (LLVMPointerType w) ->
      Alignment ->
      UndefinedBehavior e
  
    -- -------------------------------- Pointer arithmetic
  
    PtrAddOffsetOutOfBounds ::
      (1 <= w) =>
      e (LLVMPointerType w) ->
      e (BVType w) ->
      UndefinedBehavior e
  
    -- | Arguments: kind of comparison, the invalid pointer, the other pointer
    CompareInvalidPointer ::
      (1 <= w) =>
      PtrComparisonOperator ->
      e (LLVMPointerType w) ->
      e (LLVMPointerType w) ->
      UndefinedBehavior e
  
    -- | "In all other cases, the behavior is undefined"
    -- TODO: 'PtrComparisonOperator' argument?
    CompareDifferentAllocs ::
      (1 <= w) =>
      e (LLVMPointerType w) ->
      e (LLVMPointerType w) ->
      UndefinedBehavior e
  
    -- | "When two pointers are subtracted, both shall point to elements of the
    -- same array object"
    PtrSubDifferentAllocs ::
      (1 <= w) =>
      e (LLVMPointerType w) ->
      e (LLVMPointerType w) ->
      UndefinedBehavior e
  
    -- | Pointer cast to an integer type other than
    --   pointer width integers
    PointerIntCast ::
      (1 <= w) =>
      e (LLVMPointerType w) ->
      StorageType ->
      UndefinedBehavior e
  
    -- | Pointer used in an unsupported arithmetic or bitvector operation
    PointerUnsupportedOp ::
      (1 <= w) =>
      e (LLVMPointerType w) ->
      String ->
      UndefinedBehavior e
  
    -- | Pointer cast to a floating-point type
    PointerFloatCast ::
      (1 <= w) =>
      e (LLVMPointerType w) ->
      StorageType ->
      UndefinedBehavior e
  
    -- | "One of the following shall hold: [...] one operand is a pointer and the
    -- other is a null pointer constant."
    ComparePointerToBV ::
      (1 <= w) =>
      e (LLVMPointerType w) ->
      e (BVType w) ->
      UndefinedBehavior e
  
    -------------------------------- Division operators
  
    -- | @SymBV@ or @Expr _ _ (BVType w)@
    UDivByZero   :: (1 <= w) => e (BVType w) -> e (BVType w) -> UndefinedBehavior e
    SDivByZero   :: (1 <= w) => e (BVType w) -> e (BVType w) -> UndefinedBehavior e
    URemByZero   :: (1 <= w) => e (BVType w) -> e (BVType w) -> UndefinedBehavior e
    SRemByZero   :: (1 <= w) => e (BVType w) -> e (BVType w) -> UndefinedBehavior e
    SDivOverflow :: (1 <= w) => e (BVType w) -> e (BVType w) -> UndefinedBehavior e
    SRemOverflow :: (1 <= w) => e (BVType w) -> e (BVType w) -> UndefinedBehavior e
  
    -------------------------------- Integer arithmetic
  
    AbsIntMin    :: (1 <= w) => e (BVType w) -> UndefinedBehavior e
  
    PoisonValueCreated ::
      Poison.Poison e ->
      UndefinedBehavior e
  
    {-
    MemcpyDisjoint          :: UndefinedBehavior e
    DereferenceBadAlignment :: UndefinedBehavior e
    ModifiedStringLiteral   :: UndefinedBehavior e
    -}
    deriving (Typeable)
  
  -- | Which document prohibits this behavior?
  standard :: UndefinedBehavior e -> Standard
  standard =
    \case
  
      -- -------------------------------- Memory management
  
      DoubleFree{}              -> CStd C11
      FreeBadOffset{}           -> CStd C11
      FreeUnallocated{}         -> CStd C11
      MemsetInvalidRegion{}     -> CStd C11
      ReadBadAlignment{}        -> CStd C11
      WriteBadAlignment{}       -> CStd C11
  
      -- -------------------------------- Pointer arithmetic
  
      PtrAddOffsetOutOfBounds{} -> CStd C11
      CompareInvalidPointer{}   -> CStd C11
      CompareDifferentAllocs{}  -> CStd C11
      PtrSubDifferentAllocs{}   -> CStd C11
      ComparePointerToBV{}      -> CStd C11
      PointerFloatCast{}        -> CStd C11
      PointerIntCast{}          -> CStd C11
      PointerUnsupportedOp{}    -> CStd C11
  
      -- -------------------------------- Division operators
  
      UDivByZero{}   -> CStd C11
      SDivByZero{}   -> CStd C11
      URemByZero{}   -> CStd C11
      SRemByZero{}   -> CStd C11
      SDivOverflow{} -> CStd C11
      SRemOverflow{} -> CStd C11
  
      -- -------------------------------- Integer arithmetic
  
      AbsIntMin{}    -> CStd C11
  
      PoisonValueCreated p -> Poison.standard p
  
      {-
      MemcpyDisjoint          -> CStd C11
      DereferenceBadAlignment -> CStd C11
      ModifiedStringLiteral   -> CStd C11
      -}
  
  -- | Which section(s) of the document prohibit this behavior?
  cite :: UndefinedBehavior e -> Doc ann
  cite =
    \case
  
      -------------------------------- Memory management
  
      FreeBadOffset{}           -> "§7.22.3.3 The free function, ¶2"
      FreeUnallocated{}         -> "§7.22.3.3 The free function, ¶2"
      DoubleFree{}              -> "§7.22.3.3 The free function, ¶2"
      MemsetInvalidRegion{}     -> "§7.24.1 String function conventions, ¶1"
      ReadBadAlignment{}        -> "§6.5.3.2 Address and indirection operators, ¶4"
      WriteBadAlignment{}       -> "§6.5.3.2 Address and indirection operators, ¶4"
  
      ---------------------------------- Pointer arithmetic
  
      PtrAddOffsetOutOfBounds{} -> "§6.5.6 Additive operators, ¶8"
      CompareInvalidPointer{}   -> "§6.5.8 Relational operators, ¶5"
      CompareDifferentAllocs{}  -> "§6.5.8 Relational operators, ¶5"
      PtrSubDifferentAllocs{}   -> "§6.5.6 Additive operators, ¶9"
      ComparePointerToBV{}      -> "§6.5.9 Equality operators, ¶2"
      PointerFloatCast{}        -> "§6.5.4 Cast operators, ¶4"
      PointerIntCast{}          -> "§6.3.2.3 Conversions, pointers, ¶6"
      PointerUnsupportedOp{}    -> "§6.3.2.3 Conversions, pointers, ¶6"
  
      -------------------------------- Division operators
  
      UDivByZero{}   -> "§6.5.5 Multiplicitive operators, ¶5"
      SDivByZero{}   -> "§6.5.5 Multiplicitive operators, ¶5"
      URemByZero{}   -> "§6.5.5 Multiplicitive operators, ¶5"
      SRemByZero{}   -> "§6.5.5 Multiplicitive operators, ¶5"
      SDivOverflow{} -> "§6.5.5 Multiplicitive operators, ¶6"
      SRemOverflow{} -> "§6.5.5 Multiplicitive operators, ¶6"
  
      -------------------------------- Integer arithmetic
  
      AbsIntMin{} -> "§7.22.6 Integer arithmetic functions, ¶1"
  
      PoisonValueCreated p -> Poison.cite p
  
      -------------------------------- Other
  
      {-
      MemcpyDisjoint          -> "§7.24.2.1 The memcpy function"
      DereferenceBadAlignment -> "§6.5.3.2 Address and indirection operators"
      ModifiedStringLiteral   -> "§J.2 Undefined behavior" -- 6.4.5
      -}
  
  -- | What happened, and why is it a problem?
  --
  -- This is a generic explanation that doesn't use the included data.
  explain :: UndefinedBehavior e -> Doc ann
  explain =
    \case
  
      -- -------------------------------- Memory management
  
      FreeBadOffset _ -> cat $
        [ "`free` called on pointer that was not previously returned by `malloc`"
        , "`calloc`, or another memory management function (the pointer did not"
        , "point to the base of an allocation, its offset should be 0)"
        ]
      FreeUnallocated _ ->
        "`free` called on pointer that didn't point to a live region of the heap"
      DoubleFree{} -> "`free` called on a pointer to already-freed memory"
      MemsetInvalidRegion{} ->
        "Pointer passed to `memset` didn't point to a mutable allocation with enough space"
      WriteBadAlignment _ _ ->
        "Wrote a value into a pointer with insufficent alignment"
      ReadBadAlignment _ _ ->
        "Read a value from a pointer with insufficent alignment"
  
      -- -------------------------------- Pointer arithmetic
  
      PtrAddOffsetOutOfBounds _ _ ->
        "Addition of an offset to a pointer resulted in a pointer to an address outside of the allocation"
      CompareInvalidPointer{} ->
        "Comparison of a pointer which wasn't null or a pointer to a live heap object"
      CompareDifferentAllocs _ _ ->
        "Comparison of pointers from different allocations"
      PtrSubDifferentAllocs _ _ ->
        "Subtraction of pointers from different allocations"
      ComparePointerToBV _ _ ->
        "Comparison of a pointer to a non zero (null) integer value"
      PointerFloatCast{} ->
        "Cast of a pointer to a floating-point type"
      PointerIntCast{} ->
        "Cast of a pointer to an incompatible integer type"
      PointerUnsupportedOp{} ->
        "Pointer cast to an integer used in an unsupported operation"
  
      -------------------------------- Division operators
  
      UDivByZero{}   -> "Unsigned division by zero"
      SDivByZero{}   -> "Signed division by zero"
      URemByZero{}   -> "Unsigned division by zero via remainder"
      SRemByZero{}   -> "Signed division by zero via remainder"
      SDivOverflow{} -> "Overflow during signed division"
      SRemOverflow{} -> "Overflow during signed division (via signed remainder)"
  
      -------------------------------- Integer arithmetic
  
      AbsIntMin{} -> "`abs`, `labs`, or `llabs` called on `INT_MIN`"
  
      PoisonValueCreated p -> vcat [ "Poison value created", Poison.explain p ]
  
      -------------------------------- Other
  
      {-
      MemcpyDisjoint     -> "Use of `memcpy` with non-disjoint regions of memory"
      DereferenceBadAlignment ->
        "Dereferenced a pointer to a type with the wrong alignment"
      ModifiedStringLiteral -> "Modified the underlying array of a string literal"
      -}
  
  -- | Pretty-print the additional information held by the constructors
  -- (for symbolic expressions)
  details :: W4I.IsExpr (W4I.SymExpr sym)
          => UndefinedBehavior (RegValue' sym)
          -> [Doc ann]
  details =
    \case
  
      -------------------------------- Memory management
  
      FreeBadOffset ptr   -> [ ppPtr1 ptr ]
      FreeUnallocated ptr -> [ ppPtr1 ptr ]
      DoubleFree ptr -> [ ppPtr1 ptr ]
      MemsetInvalidRegion destPtr fillByte len ->
        [ "Destination pointer:" <+> ppPtr1 destPtr
        , "Fill byte:          " <+> (W4I.printSymExpr $ unRV fillByte)
        , "Length:             " <+> (W4I.printSymExpr $ unRV len)
        ]
      WriteBadAlignment ptr alignment ->
        -- TODO: replace viaShow when we have instance Pretty Bytes
        [ "Required alignment:" <+> viaShow (fromAlignment alignment) <+> "bytes"
        , ppPtr1 ptr
        ]
      ReadBadAlignment ptr alignment ->
        -- TODO: replace viaShow when we have instance Pretty Bytes
        [ "Required alignment:" <+> viaShow (fromAlignment alignment) <+> "bytes"
        , ppPtr1 ptr
        ]
  
      -------------------------------- Pointer arithmetic
  
      PtrAddOffsetOutOfBounds ptr offset ->
        [ ppPtr1 ptr
        , ppOffset (unRV offset)
        ]
      CompareInvalidPointer comparison invalid other ->
        [ "Comparison:                    " <+> ppPtrComparison comparison
        , "Invalid pointer:               " <+> ppPtr (unRV invalid)
        , "Other (possibly valid) pointer:" <+> ppPtr (unRV other)
        ]
      CompareDifferentAllocs ptr1 ptr2 -> [ ppPtr2 ptr1 ptr2 ]
      PtrSubDifferentAllocs ptr1 ptr2  -> [ ppPtr2 ptr1 ptr2 ]
      ComparePointerToBV ptr bv ->
        [ ppPtr1 ptr
        , "Bitvector:" <+> (W4I.printSymExpr $ unRV bv)
        ]
      PointerFloatCast ptr castType ->
        [ ppPtr1 ptr
        , "Cast to:" <+> viaShow castType
        ]
      PointerIntCast ptr castType ->
        [ ppPtr1 ptr
        , "Cast to:" <+> viaShow castType
        ]
      PointerUnsupportedOp ptr msg ->
        [ ppPtr1 ptr
        , pretty msg
        ]
  
      -------------------------------- Division operators
  
      -- The cases are manually listed to prevent unintentional fallthrough if a
      -- constructor is added.
      UDivByZero v1 v2   -> [ ppBV2 v1 v2 ]
      SDivByZero v1 v2   -> [ ppBV2 v1 v2 ]
      URemByZero v1 v2   -> [ ppBV2 v1 v2 ]
      SRemByZero v1 v2   -> [ ppBV2 v1 v2 ]
      SDivOverflow v1 v2 -> [ ppBV2 v1 v2 ]
      SRemOverflow v1 v2 -> [ ppBV2 v1 v2 ]
  
      -------------------------------- Integer arithmetic
  
      AbsIntMin v -> [ ppBV1 v ]
  
      PoisonValueCreated p -> Poison.details p
  
    where ppBV1 :: W4I.IsExpr (W4I.SymExpr sym) =>
                   RegValue' sym (BVType w) -> Doc ann
          ppBV1 (RV bv) = "op:" <+> W4I.printSymExpr bv
  
          ppBV2 :: W4I.IsExpr (W4I.SymExpr sym) =>
                   RegValue' sym (BVType w) -> RegValue' sym (BVType w) -> Doc ann
          ppBV2 (RV bv1) (RV bv2) =
            vcat [ "op1: " <+> W4I.printSymExpr bv1
                 , "op2: " <+> W4I.printSymExpr bv2
                 ]
  
          ppPtr1 :: W4I.IsExpr (W4I.SymExpr sym) => RegValue' sym (LLVMPointerType w) -> Doc ann
          ppPtr1 (RV p) = "Pointer:" <+> ppPtr p
  
          ppPtr2 (RV ptr1) (RV ptr2) =
            vcat [ "Pointer 1:" <+>  ppPtr ptr1
                 , "Pointer 2:" <+>  ppPtr ptr2
                 ]
  
          ppOffset :: W4I.IsExpr e => e (BaseBVType w) -> Doc ann
          ppOffset = ("Offset:" <+>) . W4I.printSymExpr
  
  pp :: (UndefinedBehavior e -> [Doc ann]) -- ^ Printer for constructor data
     -> UndefinedBehavior e
     -> Doc ann
  pp extra ub = vcat (explain ub : extra ub ++ ppCitation ub)
  
  -- | Pretty-printer for symbolic backends
  ppDetails ::
    W4I.IsExpr (W4I.SymExpr sym) =>
    UndefinedBehavior (RegValue' sym) ->
    Doc ann
  ppDetails ub = vcat (details ub ++ ppCitation ub)
  
  ppCitation :: UndefinedBehavior e -> [Doc ann]
  ppCitation ub =
     (cat [ "Reference: "
          , indent 2 (pretty (ppStd (standard ub)))
          , indent 2 (cite ub)
          ]
      : case stdURL (standard ub) of
          Just url -> [ indent 2 ("Document URL:" <+> pretty url) ]
          Nothing  -> [])
  
  -- -----------------------------------------------------------------------
  -- ** Instances
  
  $(return [])
  
  instance TestEqualityC UndefinedBehavior where
    testEqualityC subterms x y = isJust $
      $(U.structuralTypeEquality [t|UndefinedBehavior|]
         [ ( U.DataArg 0 `U.TypeApp` U.AnyType
           , [| subterms |]
           )
         , ( U.ConType [t|Poison.Poison|] `U.TypeApp` U.AnyType
           , [| \a b -> if testEqualityC subterms a b then Just Refl else Nothing |]
           )
         ]
       ) x y
  
  instance OrdC UndefinedBehavior where
    compareC subterms ub1 ub2 = toOrdering $
      $(U.structuralTypeOrd [t|UndefinedBehavior|]
         [ ( U.DataArg 0 `U.TypeApp` U.AnyType
           , [| subterms |]
           )
         , ( U.ConType [t|Poison.Poison|] `U.TypeApp` U.AnyType
           , [| \a b -> fromOrdering (compareC subterms a b) |]
           )
         ]
       ) ub1 ub2
  
  instance FunctorF UndefinedBehavior where
    fmapF = TF.fmapFDefault
  
  instance FoldableF UndefinedBehavior where
    foldMapF = TF.foldMapFDefault
  
  instance TraversableF UndefinedBehavior where
    traverseF subterms =
      $(U.structuralTraversal [t|UndefinedBehavior|]
         [ ( U.DataArg 0 `U.TypeApp` U.AnyType
           , [| \_ x -> subterms x |]
           )
         , ( U.ConType [t|Poison.Poison|] `U.TypeApp` U.AnyType
           , [| \_ x -> traverseF subterms x |]
           )
         ]
       ) subterms
  
  
  concUB :: forall sym.
    W4I.IsExprBuilder sym =>
    sym ->
    (forall tp. W4I.SymExpr sym tp -> IO (GroundValue tp)) ->
    UndefinedBehavior (RegValue' sym) -> IO (UndefinedBehavior (RegValue' sym))
  concUB sym conc ub =
    let bv :: forall w. (1 <= w) => RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
        bv (RV x) = RV <$> concBV sym conc x in
    case ub of
      FreeBadOffset ptr ->
        FreeBadOffset <$> concPtr' sym conc ptr
      FreeUnallocated ptr ->
        FreeUnallocated <$> concPtr' sym conc ptr
      DoubleFree ptr ->
        DoubleFree <$> concPtr' sym conc ptr
      MemsetInvalidRegion ptr val len ->
        MemsetInvalidRegion <$> concPtr' sym conc ptr <*> bv val <*> bv len
      ReadBadAlignment ptr a ->
        ReadBadAlignment <$> concPtr' sym conc ptr <*> pure a
      WriteBadAlignment ptr a ->
        WriteBadAlignment <$> concPtr' sym conc ptr <*> pure a
  
      PtrAddOffsetOutOfBounds ptr off ->
        PtrAddOffsetOutOfBounds <$> concPtr' sym conc ptr <*> bv off
      CompareInvalidPointer op p1 p2 ->
        CompareInvalidPointer op <$> concPtr' sym conc p1 <*> concPtr' sym conc p2
      CompareDifferentAllocs p1 p2 ->
        CompareDifferentAllocs <$> concPtr' sym conc p1 <*> concPtr' sym conc p2
      PtrSubDifferentAllocs p1 p2 ->
        PtrSubDifferentAllocs <$> concPtr' sym conc p1 <*> concPtr' sym conc p2
      PointerFloatCast ptr tp ->
        PointerFloatCast <$> concPtr' sym conc ptr <*> pure tp
      PointerIntCast ptr tp ->
        PointerIntCast <$> concPtr' sym conc ptr <*> pure tp
      PointerUnsupportedOp ptr msg ->
        PointerUnsupportedOp <$> concPtr' sym conc ptr <*> pure msg
      ComparePointerToBV ptr val ->
        ComparePointerToBV <$> concPtr' sym conc ptr <*> bv val
      UDivByZero v1 v2 ->
        UDivByZero <$> bv v1 <*> bv v2
      SDivByZero v1 v2 ->
        SDivByZero <$> bv v1 <*> bv v2
      URemByZero v1 v2 ->
        URemByZero <$> bv v1 <*> bv v2
      SRemByZero v1 v2 ->
        SRemByZero <$> bv v1 <*> bv v2
      SDivOverflow v1 v2 ->
        SDivOverflow <$> bv v1 <*> bv v2
      SRemOverflow v1 v2 ->
        SRemOverflow <$> bv v1 <*> bv v2
      AbsIntMin v ->
        AbsIntMin <$> bv v
  
      PoisonValueCreated poison ->
        PoisonValueCreated <$> Poison.concPoison sym conc poison
  