Pointer.hs

------------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.LLVM.MemModel.Pointer
-- Description      : Representation of pointers in the LLVM memory model
-- Copyright        : (c) Galois, Inc 2015-2016
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
------------------------------------------------------------------------

{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}

module Lang.Crucible.LLVM.MemModel.Pointer
  ( -- * Pointer bitwidth
    HasPtrWidth
  , pattern PtrWidth
  , withPtrWidth

    -- * Crucible pointer representation
  , LLVMPointerType
  , LLVMPtr
  , SomePointer(..)
  , pattern LLVMPointerRepr
  , pattern PtrRepr
  , pattern SizeT
  , pattern LLVMPointer
  , ptrWidth
  , llvmPointerView
  , llvmPointerBlock
  , llvmPointerOffset
  , llvmPointerType
  , muxLLVMPtr
  , llvmPointer_bv
  , mkNullPointer

    -- * Concretization
  , ConcLLVMPtr(..)
  , concLLVMPtr
  , concLLVMPtrToSymbolic
  , concBV
  , concPtr
  , concPtr'
  , concPtrFn
  , concPtrFnMap
  , concToSymPtrFn
  , concToSymPtrFnMap

    -- * Operations on valid pointers
  , constOffset
  , ptrSameAlloc
  , ptrEq
  , ptrLe
  , ptrAdd
  , ptrDiff
  , ptrSub
  , ptrIsBv
  , ptrIsNull
  , isGlobalPointer
  , isGlobalPointer'

    -- * Pretty printing
  , ppPtr

    -- * Annotation
  , annotatePointerBlock
  , annotatePointerOffset
  ) where

import           Control.Monad ((<=<), guard)
import           Data.Map (Map)
import qualified Data.Map as Map (lookup)
import           Numeric.Natural
import           Prettyprinter

import           GHC.TypeLits (TypeError, ErrorMessage(..))
import           GHC.TypeNats

import qualified Data.BitVector.Sized as BV
import           Data.Parameterized.Classes
import qualified Data.Parameterized.Context as Ctx
import qualified Data.Parameterized.Map as MapF
import           Data.Parameterized.NatRepr
import qualified Text.LLVM.AST as L

import qualified What4.Expr.GroundEval as W4GE
import           What4.Interface
import           What4.InterpretedFloatingPoint
import           What4.Expr (GroundValue)

import           Lang.Crucible.Backend
import qualified Lang.Crucible.Concretize as Conc
import           Lang.Crucible.Panic (panic)
import           Lang.Crucible.Simulator.RegMap
import           Lang.Crucible.Simulator.Intrinsics
import           Lang.Crucible.Types
import qualified Lang.Crucible.LLVM.Bytes as G
import           Lang.Crucible.LLVM.Types
import           Lang.Crucible.LLVM.MemModel.Options



data LLVMPointer sym w =
  -- |A pointer is a base point offset.
  LLVMPointer (SymNat sym) (SymBV sym w)

deriving instance (Show (SymNat sym), Show (SymBV sym w)) => Show (LLVMPointer sym w)

-- | Retrieve this pointer\'s block number.
--
-- Use of this function is discouraged, as it is abstraction-breaking.
llvmPointerBlock :: LLVMPtr sym w -> SymNat sym
llvmPointerBlock (LLVMPointer blk _) = blk

-- | Retrieve this pointer\'s offset.
--
-- Use of this function is discouraged, as it is abstraction-breaking.
llvmPointerOffset :: LLVMPtr sym w -> SymBV sym w
llvmPointerOffset (LLVMPointer _ off) = off

llvmPointerType :: IsExpr (SymExpr sym) => LLVMPtr sym w -> TypeRepr (LLVMPointerType w)
llvmPointerType ptr =
  case exprType (llvmPointerOffset ptr) of
    BaseBVRepr w -> LLVMPointerRepr w

-- | Type family defining how @LLVMPointerType@ unfolds.
type family LLVMPointerImpl sym ctx where
  LLVMPointerImpl sym (EmptyCtx ::> BVType w) = LLVMPointer sym w
  LLVMPointerImpl sym ctx = TypeError ('Text "LLVM_pointer expects a single argument of BVType, but was given" ':<>:
                                       'ShowType ctx)

-- | A pointer with an existentially-quantified width
data SomePointer sym = forall w. (1 <= w) => SomePointer !(LLVMPtr sym w)

instance (IsSymInterface sym) => IntrinsicClass sym "LLVM_pointer" where
  type Intrinsic sym "LLVM_pointer" ctx = LLVMPointerImpl sym ctx

  muxIntrinsic sym _iTypes _nm (Ctx.Empty Ctx.:> (BVRepr _w)) = muxLLVMPtr sym
  muxIntrinsic _ _ nm ctx = typeError nm ctx

-- | Alternative to the 'LLVMPointer' pattern synonym, this function can be used as a view
--   constructor instead to silence incomplete pattern warnings.
llvmPointerView :: LLVMPtr sym w -> (SymNat sym, SymBV sym w)
llvmPointerView (LLVMPointer blk off) = (blk, off)

-- | Compute the width of a pointer value.
ptrWidth :: IsExprBuilder sym => LLVMPtr sym w -> NatRepr w
ptrWidth (LLVMPointer _blk bv) = bvWidth bv

-- | Convert a raw bitvector value into an LLVM pointer value.
llvmPointer_bv :: IsSymInterface sym => sym -> SymBV sym w -> IO (LLVMPtr sym w)
llvmPointer_bv sym bv =
  do blk0 <- natLit sym 0
     return (LLVMPointer blk0 bv)

-- | Produce the distinguished null pointer value.
mkNullPointer :: (1 <= w, IsSymInterface sym) => sym -> NatRepr w -> IO (LLVMPtr sym w)
mkNullPointer sym w = llvmPointer_bv sym =<< bvZero sym w

-- | A concrete LLVM pointer
data ConcLLVMPtr w
  = ConcLLVMPtr
    { -- | Concrete block number
      concBlock :: Integer
      -- | Concrete offset
    , concOffset :: BV.BV w
    , concWidth :: NatRepr w
    }

-- | Concretize a symbolic pointer to a particular 'ConcLLVMPtr' that is
-- feasible in a model.
concLLVMPtr ::
  IsExprBuilder sym =>
  -- | Model from SMT solver
  (forall tp. SymExpr sym tp -> IO (GroundValue tp)) ->
  RegValue sym (LLVMPointerType w) ->
  IO (ConcLLVMPtr w)
concLLVMPtr conc (LLVMPointer blk off) =
  do concBlk <- conc (natToIntegerPure blk)
     concOff <- conc off
     pure (ConcLLVMPtr concBlk concOff (bvWidth off))

-- | Create a symbolic pointer from a concrete one
concLLVMPtrToSymbolic ::
  (IsExprBuilder sym, 1 <= w) =>
  sym ->
  ConcLLVMPtr w ->
  IO (RegValue sym (LLVMPointerType w))
concLLVMPtrToSymbolic sym (ConcLLVMPtr concBlk concOff w) = do
  symBlk <- integerToNat sym =<< intLit sym concBlk
  symOff <- bvLit sym w concOff
  pure (LLVMPointer symBlk symOff)

concBV ::
  (IsExprBuilder sym, 1 <= w) =>
  sym ->
  (forall tp. SymExpr sym tp -> IO (GroundValue tp)) ->
  SymBV sym w -> IO (SymBV sym w)
concBV sym conc bv =
  do bv' <- conc bv
     bvLit sym (bvWidth bv) bv'

concPtr ::
  (IsExprBuilder sym, 1 <= w) =>
  sym ->
  (forall tp. SymExpr sym tp -> IO (GroundValue tp)) ->
  RegValue sym (LLVMPointerType w) ->
  IO (RegValue sym (LLVMPointerType w))
concPtr sym conc = concLLVMPtrToSymbolic sym <=< concLLVMPtr conc

concPtr' ::
  (IsExprBuilder sym, 1 <= w) =>
  sym ->
  (forall tp. SymExpr sym tp -> IO (GroundValue tp)) ->
  RegValue' sym (LLVMPointerType w) ->
  IO (RegValue' sym (LLVMPointerType w))
concPtr' sym conc (RV ptr) = RV <$> concPtr sym conc ptr

type instance Conc.ConcIntrinsic "LLVM_pointer" (EmptyCtx ::> BVType w) = ConcLLVMPtr w

-- | An 'Conc.IntrinsicConcFn' for LLVM pointers
concPtrFn :: Conc.IntrinsicConcFn t "LLVM_pointer"
concPtrFn = Conc.IntrinsicConcFn $ \ctx tyCtx ptr ->
  case Ctx.viewAssign tyCtx of
    Ctx.AssignExtend (Ctx.viewAssign -> Ctx.AssignEmpty) (BVRepr _) ->
      let W4GE.GroundEvalFn ge = Conc.model ctx
      in concLLVMPtr ge ptr
    -- These are impossible by the definition of LLVMPointerImpl
    Ctx.AssignEmpty ->
       panic "LLVM.MemModel.Pointer.concPtrFn"
         [ "Impossible: LLVMPointerType empty context" ]
    Ctx.AssignExtend _ _ ->
       panic "LLVM.MemModel.Pointer.concPtrFn"
         [ "Impossible: LLVMPointerType ill-formed context" ]

-- | A singleton map suitable for use in a 'Conc.ConcCtx' if LLVM pointers are
-- the only intrinsic type in use
concPtrFnMap :: MapF.MapF SymbolRepr (Conc.IntrinsicConcFn t)
concPtrFnMap = MapF.singleton (knownSymbol @"LLVM_pointer") concPtrFn

-- | A 'Conc.IntrinsicConcToSymFn' for LLVM pointers
concToSymPtrFn :: Conc.IntrinsicConcToSymFn "LLVM_pointer"
concToSymPtrFn = Conc.IntrinsicConcToSymFn $ \sym tyCtx ptr ->
  case Ctx.viewAssign tyCtx of
    Ctx.AssignExtend (Ctx.viewAssign -> Ctx.AssignEmpty) (BVRepr _) ->
      concLLVMPtrToSymbolic sym ptr
    -- These are impossible by the definition of LLVMPointerImpl
    Ctx.AssignEmpty ->
       panic "LLVM.MemModel.Pointer.concToSymPtrFn"
         [ "Impossible: LLVMPointerType empty context" ]
    Ctx.AssignExtend _ _ ->
       panic "LLVM.MemModel.Pointer.concToSymPtrFn"
         [ "Impossible: LLVMPointerType ill-formed context" ]

-- | A singleton map suitable for use in 'Crucible.Concretize.concToSym' if LLVM
-- pointers are the only intrinsic type in use
concToSymPtrFnMap :: MapF.MapF SymbolRepr Conc.IntrinsicConcToSymFn
concToSymPtrFnMap = MapF.singleton (knownSymbol @"LLVM_pointer") concToSymPtrFn

-- | Mux function specialized to LLVM pointer values.
muxLLVMPtr ::
  (1 <= w) =>
  IsSymInterface sym =>
  sym ->
  Pred sym ->
  LLVMPtr sym w ->
  LLVMPtr sym w ->
  IO (LLVMPtr sym w)
muxLLVMPtr sym p (LLVMPointer b1 off1) (LLVMPointer b2 off2) =
  do b   <- natIte sym p b1 b2
     off <- bvIte sym p off1 off2
     return $ LLVMPointer b off

data FloatSize (fi :: FloatInfo) where
  SingleSize :: FloatSize SingleFloat
  DoubleSize :: FloatSize DoubleFloat

deriving instance Eq (FloatSize fi)

deriving instance Ord (FloatSize fi)

deriving instance Show (FloatSize fi)

instance TestEquality FloatSize where
  testEquality SingleSize SingleSize = Just Refl
  testEquality DoubleSize DoubleSize = Just Refl
  testEquality _ _ = Nothing

-- | Generate a concrete offset value from an @Addr@ value.
constOffset :: (1 <= w, IsExprBuilder sym) => sym -> NatRepr w -> G.Addr -> IO (SymBV sym w)
constOffset sym w x = bvLit sym w (G.bytesToBV w x)

-- | Test whether two pointers point to the same allocation (i.e., have the same
-- block number).
--
-- Using this function is preferred to pattern matching on 'LLVMPointer' or
-- 'llvmPointerBlock', because it operates at a higher level of abstraction
-- (i.e., if the representation of pointers were changed, it could continue to
-- work as intended).
ptrSameAlloc ::
  (1 <= w, IsSymInterface sym) =>
  sym ->
  LLVMPtr sym w ->
  LLVMPtr sym w ->
  IO (Pred sym)
ptrSameAlloc sym (LLVMPointer base1 _off1) (LLVMPointer base2 _off2) =
  natEq sym base1 base2

-- | Test whether two pointers are equal.
ptrEq :: (1 <= w, IsSymInterface sym)
      => sym
      -> NatRepr w
      -> LLVMPtr sym w
      -> LLVMPtr sym w
      -> IO (Pred sym)
ptrEq sym _w (LLVMPointer base1 off1) (LLVMPointer base2 off2) =
  do p1 <- natEq sym base1 base2
     p2 <- bvEq sym off1 off2
     andPred sym p1 p2

-- | Test whether one pointer is less than or equal to the other.
--
-- The returned predicates assert (in this order):
--  * the first pointer is less than or equal to the second
--  * the comparison is valid: the pointers are to the same allocation
ptrLe :: (1 <= w, IsSymInterface sym, ?memOpts :: MemOptions)
      => sym
      -> NatRepr w
      -> LLVMPtr sym w
      -> LLVMPtr sym w
      -> IO (Pred sym, Pred sym)
ptrLe sym _w (LLVMPointer base1 off1) (LLVMPointer base2 off2)
  | laxPointerOrdering ?memOpts
  = do plt <- natLt sym base1 base2
       peq <- natEq sym base1 base2
       bvle <- bvUle sym off1 off2

       p <- orPred sym plt =<< andPred sym peq bvle
       return (p, truePred sym)

  | otherwise
  = do peq <- natEq sym base1 base2
       bvle <- bvUle sym off1 off2
       return (bvle, peq)

-- | Add an offset to a pointer.
ptrAdd :: (1 <= w, IsExprBuilder sym)
       => sym
       -> NatRepr w
       -> LLVMPtr sym w
       -> SymBV sym w
       -> IO (LLVMPtr sym w)
ptrAdd sym _w (LLVMPointer base off1) off2 =
  LLVMPointer base <$> bvAdd sym off1 off2

-- | Compute the difference between two pointers. The returned predicate asserts
-- that the pointers point into the same allocation block.
ptrDiff :: (1 <= w, IsSymInterface sym)
        => sym
        -> NatRepr w
        -> LLVMPtr sym w
        -> LLVMPtr sym w
        -> IO (SymBV sym w, Pred sym)
ptrDiff sym _w (LLVMPointer base1 off1) (LLVMPointer base2 off2) =
  (,) <$> bvSub sym off1 off2 <*> natEq sym base1 base2

-- | Subtract an offset from a pointer.
ptrSub :: (1 <= w, IsSymInterface sym)
       => sym
       -> NatRepr w
       -> LLVMPtr sym w
       -> SymBV sym w
       -> IO (LLVMPtr sym w)
ptrSub sym _w (LLVMPointer base off1) off2 =
  do diff <- bvSub sym off1 off2
     return (LLVMPointer base diff)

-- | Test if a pointer value is a bitvector (i.e., has a block number of 0)
--
-- Using this function is preferred to pattern matching on 'LLVMPointer' or
-- 'llvmPointerBlock', because it operates at a higher level of abstraction
-- (i.e., if the representation of pointers were changed, it could continue to
-- work as intended).
ptrIsBv ::
  IsSymInterface sym =>
  sym ->
  LLVMPtr sym w ->
  IO (Pred sym)
ptrIsBv sym (LLVMPointer blk _off) =
  natEq sym blk =<< natLit sym 0

-- | Test if a pointer value is the null pointer.
ptrIsNull :: (1 <= w, IsSymInterface sym)
          => sym
          -> NatRepr w
          -> LLVMPtr sym w
          -> IO (Pred sym)
ptrIsNull sym w (LLVMPointer blk off) =
  do pblk <- natEq sym blk =<< natLit sym 0
     poff <- bvEq sym off =<< bvLit sym (bvWidth off) (BV.zero w)
     andPred sym pblk poff

ppPtr :: IsExpr (SymExpr sym) => LLVMPtr sym wptr -> Doc ann
ppPtr (llvmPointerView -> (blk, bv))
  | Just 0 <- asNat blk = printSymExpr bv
  | otherwise =
     let blk_doc = printSymNat blk
         off_doc = printSymExpr bv
      in pretty "(" <> blk_doc <> pretty "," <+> off_doc <> pretty ")"

-- | Look up a pointer in the 'memImplGlobalMap' to see if it's a global.
--
-- This is best-effort and will only work if the pointer is fully concrete
-- and matches the address of the global on the nose. It is used in SAWscript
-- for friendly error messages.
isGlobalPointer ::
  forall sym w. (IsSymInterface sym) =>
  Map Natural L.Symbol {- ^ c.f. 'memImplSymbolMap' -} ->
  LLVMPtr sym w -> Maybe L.Symbol
isGlobalPointer symbolMap needle =
  do n <- asNat (llvmPointerBlock needle)
     z <- asBV (llvmPointerOffset needle)
     guard (BV.asUnsigned z == 0)
     Map.lookup n symbolMap

-- | For when you don't know @1 <= w@
isGlobalPointer' ::
  forall sym w. (IsSymInterface sym) =>
  Map Natural L.Symbol {- ^ c.f. 'memImplSymbolMap' -} ->
  LLVMPtr sym w -> Maybe L.Symbol
isGlobalPointer' symbolMap needle =
  case testLeq (knownNat :: NatRepr 1) (ptrWidth needle) of
    Nothing       -> Nothing
    Just LeqProof -> isGlobalPointer symbolMap needle

annotatePointerBlock ::
  forall sym w. (IsSymInterface sym) =>
  sym ->
  LLVMPtr sym w ->
  IO (SymAnnotation sym BaseIntegerType, LLVMPointer sym w)
annotatePointerBlock sym (LLVMPointer blk off) =
  do (annotation, annotatedBlkInt) <- annotateTerm sym =<< natToInteger sym blk
     annotatedBlkNat <- integerToNat sym annotatedBlkInt
     pure (annotation, LLVMPointer annotatedBlkNat off)

annotatePointerOffset ::
  forall sym w. (IsSymInterface sym) =>
  sym ->
  LLVMPtr sym w ->
  IO (SymAnnotation sym (BaseBVType w), LLVMPointer sym w)
annotatePointerOffset sym (LLVMPointer blk off) =
  do (annotation, annotatedOff) <- annotateTerm sym off
     pure (annotation, LLVMPointer blk annotatedOff)