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