crucible-llvm-0.10: src/Lang/Crucible/LLVM/Errors/Poison.hs
-- |
-- 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 =
\case
AddNoUnsignedWrap _ _ -> LLVMRef LLVM8
AddNoSignedWrap _ _ -> LLVMRef LLVM8
SubNoUnsignedWrap _ _ -> LLVMRef LLVM8
SubNoSignedWrap _ _ -> LLVMRef LLVM8
MulNoUnsignedWrap _ _ -> LLVMRef LLVM8
MulNoSignedWrap _ _ -> LLVMRef LLVM8
UDivExact _ _ -> LLVMRef LLVM8
SDivExact _ _ -> LLVMRef LLVM8
ShlOp2Big _ _ -> LLVMRef LLVM8
ShlNoUnsignedWrap _ _ -> LLVMRef LLVM8
ShlNoSignedWrap _ _ -> LLVMRef LLVM8
LshrExact _ _ -> LLVMRef LLVM8
LshrOp2Big _ _ -> LLVMRef LLVM8
AshrExact _ _ -> LLVMRef LLVM8
AshrOp2Big _ _ -> LLVMRef LLVM8
ExtractElementIndex _ -> LLVMRef LLVM8
InsertElementIndex _ -> LLVMRef LLVM8
LLVMAbsIntMin _ -> LLVMRef LLVM12
GEPOutOfBounds _ _ -> LLVMRef LLVM8
ZExtNonNegative _ -> LLVMRef LLVM18
UiToFpNonNegative _ -> LLVMRef LLVM19
FpToUiNotRepresentable _ _ _ -> LLVMRef LLVM8
FpToSiNotRepresentable _ _ _ -> LLVMRef LLVM8
TruncNoUnsignedWrap _ -> LLVMRef LLVM20
TruncNoSignedWrap _ -> LLVMRef LLVM20
ICmpSameSign _ _ -> LLVMRef LLVM20
-- | Which section(s) of the document state that this is poison?
cite :: Poison e -> Doc ann
cite =
\case
AddNoUnsignedWrap _ _ -> "‘add’ Instruction (Semantics)"
AddNoSignedWrap _ _ -> "‘add’ Instruction (Semantics)"
SubNoUnsignedWrap _ _ -> "‘sub’ Instruction (Semantics)"
SubNoSignedWrap _ _ -> "‘sub’ Instruction (Semantics)"
MulNoUnsignedWrap _ _ -> "‘mul’ Instruction (Semantics)"
MulNoSignedWrap _ _ -> "‘mul’ Instruction (Semantics)"
UDivExact _ _ -> "‘udiv’ Instruction (Semantics)"
SDivExact _ _ -> "‘sdiv’ Instruction (Semantics)"
ShlOp2Big _ _ -> "‘shl’ Instruction (Semantics)"
ShlNoUnsignedWrap _ _ -> "‘shl’ Instruction (Semantics)"
ShlNoSignedWrap _ _ -> "‘shl’ Instruction (Semantics)"
LshrExact _ _ -> "‘lshr’ Instruction (Semantics)"
LshrOp2Big _ _ -> "‘lshr’ Instruction (Semantics)"
AshrExact _ _ -> "‘ashr’ Instruction (Semantics)"
AshrOp2Big _ _ -> "‘ashr’ Instruction (Semantics)"
ExtractElementIndex _ -> "‘extractelement’ Instruction (Semantics)"
InsertElementIndex _ -> "‘insertelement’ Instruction (Semantics)"
LLVMAbsIntMin _ -> "‘llvm.abs.*’ Intrinsic (Semantics)"
GEPOutOfBounds _ _ -> "‘getelementptr’ Instruction (Semantics)"
ZExtNonNegative _ -> "‘zext’ Instruction (Semantics)"
UiToFpNonNegative _ -> "‘uitofp’ Instruction (Semantics)"
FpToUiNotRepresentable _ _ _ -> "‘fptoui’ Instruction (Semantics)"
FpToSiNotRepresentable _ _ _ -> "‘fptosi’ Instruction (Semantics)"
TruncNoUnsignedWrap _ -> "‘trunc’ Instruction (Semantics)"
TruncNoSignedWrap _ -> "‘trunc’ Instruction (Semantics)"
ICmpSameSign _ _ -> "‘icmp’ Instruction (Semantics)"
explain :: Poison e -> Doc ann
explain =
\case
AddNoUnsignedWrap _ _ ->
"Unsigned addition caused wrapping even though the `nuw` flag was set"
AddNoSignedWrap _ _ ->
"Signed addition caused wrapping even though the `nsw` flag was set"
SubNoUnsignedWrap _ _ ->
"Unsigned subtraction caused wrapping even though the `nuw` flag was set"
SubNoSignedWrap _ _ ->
"Signed subtraction caused wrapping even though the `nsw` flag was set"
MulNoUnsignedWrap _ _ ->
"Unsigned multiplication caused wrapping even though the `nuw` flag was set"
MulNoSignedWrap _ _ ->
"Signed multiplication caused wrapping even though the `nsw` flag was set"
SDivExact _ _ ->
"Inexact signed division even though the `exact` flag was set"
UDivExact _ _ ->
"Inexact unsigned division even though the `exact` flag was set"
ShlOp2Big _ _ ->
"The second operand of `shl` was equal to or greater than the number of bits in the first operand"
ShlNoUnsignedWrap _ _ ->
"Left shift shifted out non-zero bits even though the `nuw` flag was set"
ShlNoSignedWrap _ _ ->
"Left shift shifted out some bits that disagreed with the sign bit even though the `nsw` flag was set"
LshrExact _ _ ->
"Inexact `lshr` (logical right shift) result even though the `exact` flag was set"
LshrOp2Big _ _ ->
"The second operand of `lshr` was equal to or greater than the number of bits in the first operand"
AshrExact _ _ ->
"Inexact `ashr` (arithmetic right shift) result even though the `exact` flag was set"
AshrOp2Big _ _ ->
"The second operand of `ashr` was equal to or greater than the number of bits in the first operand"
ExtractElementIndex _ -> cat $
[ "Attempted to extract an element from a vector at an index that was"
, "greater than the length of the vector"
]
InsertElementIndex _ -> cat $
[ "Attempted to insert an element into a vector at an index that was"
, "greater than the length of the vector"
]
LLVMAbsIntMin _ -> cat $
[ "The first argument of `llvm.abs.*` was `INT_MIN` even though the"
, "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 _ _ -> cat $
[ "Calling `getelementptr` resulted in an index that was out of bounds for the"
, "given allocation (likely due to arithmetic overflow), but Crucible currently"
, "treats all GEP instructions as if they had the `inbounds` attribute set."
]
ZExtNonNegative _ ->
"A negative integer was zero-extended even though the `nneg` flag was set"
UiToFpNonNegative _ ->
"A negative integer was converted to a floating-point value even though the `nneg` flag was set"
FpToUiNotRepresentable _ _ _ -> cat $
[ "A floating-point value was converted to an unsigned integer,"
, "even though the value does not fit in the unsigned integer's type"
]
FpToSiNotRepresentable _ _ _ -> cat $
[ "A floating-point value was converted to a signed integer,"
, "even though the value does not fit in the signed integer's type"
]
TruncNoUnsignedWrap _ ->
"Unsigned truncation caused wrapping even though the `nuw` flag was set"
TruncNoSignedWrap _ ->
"Signed truncation caused wrapping even though the `nsw` flag was set"
ICmpSameSign _ _ ->
"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 =
\case
AddNoUnsignedWrap v1 v2 -> args [v1, v2]
AddNoSignedWrap v1 v2 -> args [v1, v2]
SubNoUnsignedWrap v1 v2 -> args [v1, v2]
SubNoSignedWrap v1 v2 -> args [v1, v2]
MulNoUnsignedWrap v1 v2 -> args [v1, v2]
MulNoSignedWrap v1 v2 -> args [v1, v2]
SDivExact v1 v2 -> args [v1, v2]
UDivExact v1 v2 -> args [v1, v2]
ShlOp2Big v1 v2 -> args [v1, v2]
ShlNoUnsignedWrap v1 v2 -> args [v1, v2]
ShlNoSignedWrap v1 v2 -> args [v1, v2]
LshrExact v1 v2 -> args [v1, v2]
LshrOp2Big v1 v2 -> args [v1, v2]
AshrExact v1 v2 -> args [v1, v2]
AshrOp2Big v1 v2 -> args [v1, v2]
ExtractElementIndex v -> args [v]
InsertElementIndex v -> args [v]
LLVMAbsIntMin v -> args [v]
GEPOutOfBounds (RV ptr) (RV bv) ->
[ "Pointer:" <+> ppPtr ptr
, "Bitvector:" <+> W4I.printSymExpr bv
]
ZExtNonNegative v -> args [v]
UiToFpNonNegative v -> args [v]
FpToUiNotRepresentable fi (RV float) bvW ->
[ "Floating-point type:" <+> pretty fi
, "Floating-point value:" <+> W4I.printSymExpr float
, "Unsigned integer size (in bits):" <+> viaShow bvW
]
FpToSiNotRepresentable fi (RV float) bvW ->
[ "Floating-point type:" <+> pretty fi
, "Floating-point value:" <+> W4I.printSymExpr float
, "Signed integer size (in bits):" <+> viaShow bvW
]
TruncNoUnsignedWrap v -> args [v]
TruncNoSignedWrap v -> args [v]
ICmpSameSign v1 v2 -> args [v1, v2]
where
args :: forall w. [RegValue' sym (BVType w)] -> [Doc ann]
args [] = [ "No arguments" ]
args [RV v] = [ "Argument:" <+> W4I.printSymExpr v ]
args vs = [ hsep ("Arguments:" : map (W4I.printSymExpr . unRV) 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 extra poison = vcat $
[ "Poison value encountered: "
, explain poison
, vcat (extra poison)
, cat [ "Reference: "
, pretty (ppStd (standard poison))
, cite poison
]
] ++ case stdURL (standard poison) of
Just url -> ["Document URL:" <+> pretty url]
Nothing -> []
-- | Pretty print an error message relating to LLVM poison values
ppReg ::W4I.IsExpr (W4I.SymExpr sym) => Poison (RegValue' sym) -> Doc ann
ppReg = pp 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 sym fm conc poison =
let bv :: forall w. (1 <= w) => RegValue' sym (BVType w) -> IO (RegValue' sym (BVType w))
bv (RV x) = RV <$> concBV sym conc x
fp ::
forall fi.
FloatInfoRepr fi ->
RegValue' sym (FloatType fi) ->
IO (RegValue' sym (FloatType fi))
fp fi (RV x) = do
v <- conc x
rv <-
case fm of
FloatIEEERepr ->
W4I.floatLit sym (floatInfoToPrecisionRepr fi) v
FloatUninterpretedRepr -> do
sv <- W4GE.groundToSym sym (floatInfoToBVTypeRepr fi) v
W4IFP.iFloatFromBinary sym fi sv
FloatRealRepr ->
W4IFP.iFloatLitRational sym fi v
pure $ RV rv in
case poison of
AddNoUnsignedWrap v1 v2 ->
AddNoUnsignedWrap <$> bv v1 <*> bv v2
AddNoSignedWrap v1 v2 ->
AddNoSignedWrap <$> bv v1 <*> bv v2
SubNoUnsignedWrap v1 v2 ->
SubNoUnsignedWrap <$> bv v1 <*> bv v2
SubNoSignedWrap v1 v2 ->
SubNoSignedWrap <$> bv v1 <*> bv v2
MulNoUnsignedWrap v1 v2 ->
MulNoUnsignedWrap<$> bv v1 <*> bv v2
MulNoSignedWrap v1 v2 ->
MulNoSignedWrap <$> bv v1 <*> bv v2
UDivExact v1 v2 ->
UDivExact <$> bv v1 <*> bv v2
SDivExact v1 v2 ->
SDivExact <$> bv v1 <*> bv v2
ShlOp2Big v1 v2 ->
ShlOp2Big <$> bv v1 <*> bv v2
ShlNoUnsignedWrap v1 v2 ->
ShlNoUnsignedWrap <$> bv v1 <*> bv v2
ShlNoSignedWrap v1 v2 ->
ShlNoSignedWrap <$> bv v1 <*> bv v2
LshrExact v1 v2 ->
LshrExact <$> bv v1 <*> bv v2
LshrOp2Big v1 v2 ->
LshrOp2Big <$> bv v1 <*> bv v2
AshrExact v1 v2 ->
AshrExact <$> bv v1 <*> bv v2
AshrOp2Big v1 v2 ->
AshrOp2Big <$> bv v1 <*> bv v2
ExtractElementIndex v ->
ExtractElementIndex <$> bv v
InsertElementIndex v ->
InsertElementIndex <$> bv v
GEPOutOfBounds p v ->
GEPOutOfBounds <$> concPtr' sym conc p <*> bv v
LLVMAbsIntMin v ->
LLVMAbsIntMin <$> bv v
ZExtNonNegative v ->
ZExtNonNegative <$> bv v
UiToFpNonNegative v ->
UiToFpNonNegative <$> bv v
FpToUiNotRepresentable v1 v2 v3 ->
FpToUiNotRepresentable v1 <$> fp v1 v2 <*> pure v3
FpToSiNotRepresentable v1 v2 v3 ->
FpToSiNotRepresentable v1 <$> fp v1 v2 <*> pure v3
TruncNoUnsignedWrap v ->
TruncNoUnsignedWrap <$> bv v
TruncNoSignedWrap v ->
TruncNoSignedWrap <$> bv v
ICmpSameSign v1 v2 ->
ICmpSameSign <$> bv v1 <*> bv 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 subterms =
let subterms' :: forall p q. e p -> e q -> Maybe (() :~: ())
subterms' a b =
case subterms a b of
Just Refl -> Just Refl
Nothing -> 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 subterms =
let subterms' :: forall p q. e p -> f q -> OrderingF () ()
subterms' a b =
case subterms a b of
EQF -> (EQF :: OrderingF () ())
GTF -> (GTF :: OrderingF () ())
LTF -> (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 subterms x y = isJust $ eqcPoison subterms x y
instance OrdC Poison where
compareC subterms x y = toOrdering $ ordcPoison subterms x y
instance FunctorF Poison where
fmapF = TF.fmapFDefault
instance FoldableF Poison where
foldMapF = 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 =
$(U.structuralTraversal [t|Poison|]
[ ( U.DataArg 0 `U.TypeApp` U.AnyType
, [| ($) |] -- \f x -> f x
)
]
)