crucible-llvm-0.6: 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(..), 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 =
\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
-- | 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)"
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.
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` flag 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
]
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.
W4I.IsExprBuilder sym =>
sym ->
(forall tp. W4I.SymExpr sym tp -> IO (GroundValue tp)) ->
Poison (RegValue' sym) -> IO (Poison (RegValue' sym))
concPoison sym 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 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
-- -----------------------------------------------------------------------
-- ** 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' |])
])
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' |])
])
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
)
]
)