------------------------------------------------------------------------
-- |
-- 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 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
  , concBV
  , concPtr
  , concPtr'

    -- * Operations on valid pointers
  , constOffset
  , ptrEq
  , ptrLe
  , ptrAdd
  , ptrDiff
  , ptrSub
  , 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           Data.Parameterized.NatRepr
import qualified Text.LLVM.AST as L

import           What4.Interface
import           What4.InterpretedFloatingPoint
import           What4.Expr (GroundValue)

import           Lang.Crucible.Backend
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)

llvmPointerBlock :: LLVMPtr sym w -> SymNat sym
llvmPointerBlock :: forall sym (w :: Nat). LLVMPtr sym w -> SymNat sym
llvmPointerBlock (LLVMPointer SymNat sym
blk SymBV sym w
_) = SymNat sym
blk

llvmPointerOffset :: LLVMPtr sym w -> SymBV sym w
llvmPointerOffset :: forall sym (w :: Nat). LLVMPtr sym w -> SymBV sym w
llvmPointerOffset (LLVMPointer SymNat sym
_ SymBV sym w
off) = SymBV sym w
off

llvmPointerType :: IsExpr (SymExpr sym) => LLVMPtr sym w -> TypeRepr (LLVMPointerType w)
llvmPointerType :: forall sym (w :: Nat).
IsExpr (SymExpr sym) =>
LLVMPtr sym w -> TypeRepr (LLVMPointerType w)
llvmPointerType LLVMPtr sym w
ptr =
  case SymExpr sym (BaseBVType w) -> BaseTypeRepr (BaseBVType w)
forall (tp :: BaseType). SymExpr sym tp -> BaseTypeRepr tp
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
exprType (LLVMPtr sym w -> SymExpr sym (BaseBVType w)
forall sym (w :: Nat). LLVMPtr sym w -> SymBV sym w
llvmPointerOffset LLVMPtr sym w
ptr) of
    BaseBVRepr NatRepr w
w -> NatRepr w -> TypeRepr (LLVMPointerType w)
forall (ty :: CrucibleType) (w :: Nat).
(1 <= w, ty ~ LLVMPointerType w) =>
NatRepr w -> TypeRepr ty
LLVMPointerRepr NatRepr w
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 :: forall (ctx :: Ctx CrucibleType).
sym
-> IntrinsicTypes sym
-> SymbolRepr "LLVM_pointer"
-> CtxRepr ctx
-> Pred sym
-> Intrinsic sym "LLVM_pointer" ctx
-> Intrinsic sym "LLVM_pointer" ctx
-> IO (Intrinsic sym "LLVM_pointer" ctx)
muxIntrinsic sym
sym IntrinsicTypes sym
_iTypes SymbolRepr "LLVM_pointer"
_nm (Assignment TypeRepr ctx
Ctx.Empty Ctx.:> (BVRepr NatRepr n
_w)) = sym
-> Pred sym -> LLVMPtr sym n -> LLVMPtr sym n -> IO (LLVMPtr sym n)
forall (w :: Nat) sym.
(1 <= w, IsSymInterface sym) =>
sym
-> Pred sym -> LLVMPtr sym w -> LLVMPtr sym w -> IO (LLVMPtr sym w)
muxLLVMPtr sym
sym
  muxIntrinsic sym
_ IntrinsicTypes sym
_ SymbolRepr "LLVM_pointer"
nm Assignment TypeRepr ctx
ctx = SymbolRepr "LLVM_pointer"
-> Assignment TypeRepr ctx
-> Pred sym
-> LLVMPointerImpl sym ctx
-> LLVMPointerImpl sym ctx
-> IO (LLVMPointerImpl sym ctx)
forall (nm :: Symbol) (ctx :: Ctx CrucibleType) b.
HasCallStack =>
SymbolRepr nm -> CtxRepr ctx -> b
typeError SymbolRepr "LLVM_pointer"
nm Assignment TypeRepr ctx
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 :: forall sym (w :: Nat). LLVMPtr sym w -> (SymNat sym, SymBV sym w)
llvmPointerView (LLVMPointer SymNat sym
blk SymBV sym w
off) = (SymNat sym
blk, SymBV sym w
off)

-- | Compute the width of a pointer value.
ptrWidth :: IsExprBuilder sym => LLVMPtr sym w -> NatRepr w
ptrWidth :: forall sym (w :: Nat).
IsExprBuilder sym =>
LLVMPtr sym w -> NatRepr w
ptrWidth (LLVMPointer SymNat sym
_blk SymBV sym w
bv) = SymBV sym w -> NatRepr w
forall (w :: Nat). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
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 :: forall sym (w :: Nat).
IsSymInterface sym =>
sym -> SymBV sym w -> IO (LLVMPtr sym w)
llvmPointer_bv sym
sym SymBV sym w
bv =
  do SymNat sym
blk0 <- sym -> Nat -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Nat -> IO (SymNat sym)
natLit sym
sym Nat
0
     LLVMPointer sym w -> IO (LLVMPointer sym w)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SymNat sym -> SymBV sym w -> LLVMPointer sym w
forall sym (w :: Nat).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
LLVMPointer SymNat sym
blk0 SymBV sym w
bv)

-- | Produce the distinguished null pointer value.
mkNullPointer :: (1 <= w, IsSymInterface sym) => sym -> NatRepr w -> IO (LLVMPtr sym w)
mkNullPointer :: forall (w :: Nat) sym.
(1 <= w, IsSymInterface sym) =>
sym -> NatRepr w -> IO (LLVMPtr sym w)
mkNullPointer sym
sym NatRepr w
w = sym
-> SymExpr sym (BaseBVType w)
-> IO
     (RegValue
        sym (IntrinsicType "LLVM_pointer" (EmptyCtx '::> BVType w)))
forall sym (w :: Nat).
IsSymInterface sym =>
sym -> SymBV sym w -> IO (LLVMPtr sym w)
llvmPointer_bv sym
sym (SymExpr sym (BaseBVType w) -> IO (LLVMPointer sym w))
-> IO (SymExpr sym (BaseBVType w)) -> IO (LLVMPointer sym w)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> NatRepr w -> BV w -> IO (SymExpr sym (BaseBVType w))
forall (w :: Nat).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w (NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr w
w)


concBV ::
  (IsExprBuilder sym, 1 <= w) =>
  sym ->
  (forall tp. SymExpr sym tp -> IO (GroundValue tp)) ->
  SymBV sym w -> IO (SymBV sym w)
concBV :: forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> SymBV sym w
-> IO (SymBV sym w)
concBV sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc SymBV sym w
bv =
  do BV w
bv' <- SymBV sym w -> IO (GroundValue (BaseBVType w))
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc SymBV sym w
bv
     sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym (SymBV sym w -> NatRepr w
forall (w :: Nat). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
bv) BV w
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 :: forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue sym (LLVMPointerType w)
-> IO (RegValue sym (LLVMPointerType w))
concPtr sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (LLVMPointer SymNat sym
blk SymBV sym w
off) =
  do SymNat sym
blk' <- sym -> SymExpr sym BaseIntegerType -> IO (SymNat sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymNat sym)
integerToNat sym
sym (SymExpr sym BaseIntegerType -> IO (SymNat sym))
-> IO (SymExpr sym BaseIntegerType) -> IO (SymNat sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Integer -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
intLit sym
sym (Integer -> IO (SymExpr sym BaseIntegerType))
-> IO Integer -> IO (SymExpr sym BaseIntegerType)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< SymExpr sym BaseIntegerType -> IO Integer
SymExpr sym BaseIntegerType -> IO (GroundValue BaseIntegerType)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (SymExpr sym BaseIntegerType -> IO Integer)
-> IO (SymExpr sym BaseIntegerType) -> IO Integer
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymNat sym -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> IO (SymInteger sym)
natToInteger sym
sym SymNat sym
blk
     SymBV sym w
off' <- sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> SymBV sym w
-> IO (SymBV sym w)
concBV sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc SymBV sym w
off
     LLVMPointer sym w -> IO (LLVMPointer sym w)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SymNat sym -> SymBV sym w -> LLVMPointer sym w
forall sym (w :: Nat).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
LLVMPointer SymNat sym
blk' SymBV sym w
off')

concPtr' ::
  (IsExprBuilder sym, 1 <= w) =>
  sym ->
  (forall tp. SymExpr sym tp -> IO (GroundValue tp)) ->
  RegValue' sym (LLVMPointerType w) ->
  IO (RegValue' sym (LLVMPointerType w))
concPtr' :: forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue' sym (LLVMPointerType w)
-> IO (RegValue' sym (LLVMPointerType w))
concPtr' sym
sym forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (RV RegValue sym (LLVMPointerType w)
ptr) = RegValue sym (LLVMPointerType w)
-> RegValue' sym (LLVMPointerType w)
LLVMPointer sym w -> RegValue' sym (LLVMPointerType w)
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
RV (LLVMPointer sym w -> RegValue' sym (LLVMPointerType w))
-> IO (LLVMPointer sym w) -> IO (RegValue' sym (LLVMPointerType w))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue sym (LLVMPointerType w)
-> IO (RegValue sym (LLVMPointerType w))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym
-> (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue sym (LLVMPointerType w)
-> IO (RegValue sym (LLVMPointerType w))
concPtr sym
sym SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc RegValue sym (LLVMPointerType w)
ptr


-- | 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 :: forall (w :: Nat) sym.
(1 <= w, IsSymInterface sym) =>
sym
-> Pred sym -> LLVMPtr sym w -> LLVMPtr sym w -> IO (LLVMPtr sym w)
muxLLVMPtr sym
sym Pred sym
p (LLVMPointer SymNat sym
b1 SymBV sym w
off1) (LLVMPointer SymNat sym
b2 SymBV sym w
off2) =
  do SymNat sym
b   <- sym -> Pred sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natIte sym
sym Pred sym
p SymNat sym
b1 SymNat sym
b2
     SymBV sym w
off <- sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym Pred sym
p SymBV sym w
off1 SymBV sym w
off2
     LLVMPointer sym w -> IO (LLVMPointer sym w)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (LLVMPointer sym w -> IO (LLVMPointer sym w))
-> LLVMPointer sym w -> IO (LLVMPointer sym w)
forall a b. (a -> b) -> a -> b
$ SymNat sym -> SymBV sym w -> LLVMPointer sym w
forall sym (w :: Nat).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
LLVMPointer SymNat sym
b SymBV sym w
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 :: forall (a :: FloatInfo) (b :: FloatInfo).
FloatSize a -> FloatSize b -> Maybe (a :~: b)
testEquality FloatSize a
SingleSize FloatSize b
SingleSize = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  testEquality FloatSize a
DoubleSize FloatSize b
DoubleSize = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  testEquality FloatSize a
_ FloatSize b
_ = Maybe (a :~: b)
forall a. Maybe a
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 :: forall (w :: Nat) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> Addr -> IO (SymBV sym w)
constOffset sym
sym NatRepr w
w Addr
x = sym -> NatRepr w -> BV w -> IO (SymExpr sym (BaseBVType w))
forall (w :: Nat).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym NatRepr w
w (NatRepr w -> Addr -> BV w
forall (w :: Nat). NatRepr w -> Addr -> BV w
G.bytesToBV NatRepr w
w Addr
x)

-- | Test whether two pointers are equal.
ptrEq :: (1 <= w, IsSymInterface sym)
      => sym
      -> NatRepr w
      -> LLVMPtr sym w
      -> LLVMPtr sym w
      -> IO (Pred sym)
ptrEq :: forall (w :: Nat) sym.
(1 <= w, IsSymInterface sym) =>
sym -> NatRepr w -> LLVMPtr sym w -> LLVMPtr sym w -> IO (Pred sym)
ptrEq sym
sym NatRepr w
_w (LLVMPointer SymNat sym
base1 SymBV sym w
off1) (LLVMPointer SymNat sym
base2 SymBV sym w
off2) =
  do Pred sym
p1 <- sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natEq sym
sym SymNat sym
base1 SymNat sym
base2
     Pred sym
p2 <- sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq sym
sym SymBV sym w
off1 SymBV sym w
off2
     sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
p1 Pred sym
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 :: forall (w :: Nat) sym.
(1 <= w, IsSymInterface sym, ?memOpts::MemOptions) =>
sym
-> NatRepr w
-> LLVMPtr sym w
-> LLVMPtr sym w
-> IO (Pred sym, Pred sym)
ptrLe sym
sym NatRepr w
_w (LLVMPointer SymNat sym
base1 SymBV sym w
off1) (LLVMPointer SymNat sym
base2 SymBV sym w
off2)
  | MemOptions -> Bool
laxPointerOrdering ?memOpts::MemOptions
MemOptions
?memOpts
  = do Pred sym
plt <- sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natLt sym
sym SymNat sym
base1 SymNat sym
base2
       Pred sym
peq <- sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natEq sym
sym SymNat sym
base1 SymNat sym
base2
       Pred sym
bvle <- sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUle sym
sym SymBV sym w
off1 SymBV sym w
off2

       Pred sym
p <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
orPred sym
sym Pred sym
plt (Pred sym -> IO (Pred sym)) -> IO (Pred sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
peq Pred sym
bvle
       (Pred sym, Pred sym) -> IO (Pred sym, Pred sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym
p, sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym)

  | Bool
otherwise
  = do Pred sym
peq <- sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natEq sym
sym SymNat sym
base1 SymNat sym
base2
       Pred sym
bvle <- sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvUle sym
sym SymBV sym w
off1 SymBV sym w
off2
       (Pred sym, Pred sym) -> IO (Pred sym, Pred sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym
bvle, Pred sym
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 :: forall (w :: Nat) sym.
(1 <= w, IsExprBuilder sym) =>
sym
-> NatRepr w -> LLVMPtr sym w -> SymBV sym w -> IO (LLVMPtr sym w)
ptrAdd sym
sym NatRepr w
_w (LLVMPointer SymNat sym
base SymBV sym w
off1) SymBV sym w
off2 =
  SymNat sym -> SymBV sym w -> LLVMPointer sym w
forall sym (w :: Nat).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
LLVMPointer SymNat sym
base (SymBV sym w -> LLVMPointer sym w)
-> IO (SymBV sym w) -> IO (LLVMPointer sym w)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvAdd sym
sym SymBV sym w
off1 SymBV sym w
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 :: forall (w :: Nat) sym.
(1 <= w, IsSymInterface sym) =>
sym
-> NatRepr w
-> LLVMPtr sym w
-> LLVMPtr sym w
-> IO (SymBV sym w, Pred sym)
ptrDiff sym
sym NatRepr w
_w (LLVMPointer SymNat sym
base1 SymBV sym w
off1) (LLVMPointer SymNat sym
base2 SymBV sym w
off2) =
  (,) (SymBV sym w
 -> SymExpr sym BaseBoolType
 -> (SymBV sym w, SymExpr sym BaseBoolType))
-> IO (SymBV sym w)
-> IO
     (SymExpr sym BaseBoolType
      -> (SymBV sym w, SymExpr sym BaseBoolType))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvSub sym
sym SymBV sym w
off1 SymBV sym w
off2 IO
  (SymExpr sym BaseBoolType
   -> (SymBV sym w, SymExpr sym BaseBoolType))
-> IO (SymExpr sym BaseBoolType)
-> IO (SymBV sym w, SymExpr sym BaseBoolType)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> sym -> SymNat sym -> SymNat sym -> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natEq sym
sym SymNat sym
base1 SymNat sym
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 :: forall (w :: Nat) sym.
(1 <= w, IsSymInterface sym) =>
sym
-> NatRepr w -> LLVMPtr sym w -> SymBV sym w -> IO (LLVMPtr sym w)
ptrSub sym
sym NatRepr w
_w (LLVMPointer SymNat sym
base SymBV sym w
off1) SymBV sym w
off2 =
  do SymBV sym w
diff <- sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvSub sym
sym SymBV sym w
off1 SymBV sym w
off2
     LLVMPointer sym w -> IO (LLVMPointer sym w)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (SymNat sym -> SymBV sym w -> LLVMPointer sym w
forall sym (w :: Nat).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
LLVMPointer SymNat sym
base SymBV sym w
diff)

-- | Test if a pointer value is the null pointer.
ptrIsNull :: (1 <= w, IsSymInterface sym)
          => sym
          -> NatRepr w
          -> LLVMPtr sym w
          -> IO (Pred sym)
ptrIsNull :: forall (w :: Nat) sym.
(1 <= w, IsSymInterface sym) =>
sym -> NatRepr w -> LLVMPtr sym w -> IO (Pred sym)
ptrIsNull sym
sym NatRepr w
w (LLVMPointer SymNat sym
blk SymBV sym w
off) =
  do Pred sym
pblk <- sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> SymNat sym -> IO (Pred sym)
natEq sym
sym SymNat sym
blk (SymNat sym -> IO (Pred sym)) -> IO (SymNat sym) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> Nat -> IO (SymNat sym)
forall sym. IsExprBuilder sym => sym -> Nat -> IO (SymNat sym)
natLit sym
sym Nat
0
     Pred sym
poff <- sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq sym
sym SymBV sym w
off (SymBV sym w -> IO (Pred sym)) -> IO (SymBV sym w) -> IO (Pred sym)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit sym
sym (SymBV sym w -> NatRepr w
forall (w :: Nat). SymExpr sym (BaseBVType w) -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
bvWidth SymBV sym w
off) (NatRepr w -> BV w
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr w
w)
     sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
pblk Pred sym
poff

ppPtr :: IsExpr (SymExpr sym) => LLVMPtr sym wptr -> Doc ann
ppPtr :: forall sym (wptr :: Nat) ann.
IsExpr (SymExpr sym) =>
LLVMPtr sym wptr -> Doc ann
ppPtr (LLVMPtr sym wptr -> (SymNat sym, SymBV sym wptr)
forall sym (w :: Nat). LLVMPtr sym w -> (SymNat sym, SymBV sym w)
llvmPointerView -> (SymNat sym
blk, SymBV sym wptr
bv))
  | Just Nat
0 <- SymNat sym -> Maybe Nat
forall sym. IsExpr (SymExpr sym) => SymNat sym -> Maybe Nat
asNat SymNat sym
blk = SymBV sym wptr -> Doc ann
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr SymBV sym wptr
bv
  | Bool
otherwise =
     let blk_doc :: Doc ann
blk_doc = SymNat sym -> Doc ann
forall sym ann. IsExpr (SymExpr sym) => SymNat sym -> Doc ann
printSymNat SymNat sym
blk
         off_doc :: Doc ann
off_doc = SymBV sym wptr -> Doc ann
forall (tp :: BaseType) ann. SymExpr sym tp -> Doc ann
forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
printSymExpr SymBV sym wptr
bv
      in String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"(" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
blk_doc Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"," Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
off_doc Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
")"

-- | 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 :: forall sym (w :: Nat).
IsSymInterface sym =>
Map Nat Symbol -> LLVMPtr sym w -> Maybe Symbol
isGlobalPointer Map Nat Symbol
symbolMap LLVMPtr sym w
needle =
  do Nat
n <- SymNat sym -> Maybe Nat
forall sym. IsExpr (SymExpr sym) => SymNat sym -> Maybe Nat
asNat (LLVMPtr sym w -> SymNat sym
forall sym (w :: Nat). LLVMPtr sym w -> SymNat sym
llvmPointerBlock LLVMPtr sym w
needle)
     BV w
z <- SymExpr sym (BaseBVType w) -> Maybe (BV w)
forall (w :: Nat). SymExpr sym (BaseBVType w) -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
asBV (LLVMPtr sym w -> SymExpr sym (BaseBVType w)
forall sym (w :: Nat). LLVMPtr sym w -> SymBV sym w
llvmPointerOffset LLVMPtr sym w
needle)
     Bool -> Maybe ()
forall (f :: Type -> Type). Alternative f => Bool -> f ()
guard (BV w -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
z Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0)
     Nat -> Map Nat Symbol -> Maybe Symbol
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Nat
n Map Nat Symbol
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' :: forall sym (w :: Nat).
IsSymInterface sym =>
Map Nat Symbol -> LLVMPtr sym w -> Maybe Symbol
isGlobalPointer' Map Nat Symbol
symbolMap LLVMPtr sym w
needle =
  case NatRepr 1 -> NatRepr w -> Maybe (LeqProof 1 w)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat :: NatRepr 1) (LLVMPtr sym w -> NatRepr w
forall sym (w :: Nat).
IsExprBuilder sym =>
LLVMPtr sym w -> NatRepr w
ptrWidth LLVMPtr sym w
needle) of
    Maybe (LeqProof 1 w)
Nothing       -> Maybe Symbol
forall a. Maybe a
Nothing
    Just LeqProof 1 w
LeqProof -> Map Nat Symbol -> LLVMPtr sym w -> Maybe Symbol
forall sym (w :: Nat).
IsSymInterface sym =>
Map Nat Symbol -> LLVMPtr sym w -> Maybe Symbol
isGlobalPointer Map Nat Symbol
symbolMap LLVMPtr sym w
needle

annotatePointerBlock ::
  forall sym w. (IsSymInterface sym) =>
  sym ->
  LLVMPtr sym w ->
  IO (SymAnnotation sym BaseIntegerType, LLVMPointer sym w)
annotatePointerBlock :: forall sym (w :: Nat).
IsSymInterface sym =>
sym
-> LLVMPtr sym w
-> IO (SymAnnotation sym BaseIntegerType, LLVMPointer sym w)
annotatePointerBlock sym
sym (LLVMPointer SymNat sym
blk SymBV sym w
off) =
  do (SymAnnotation sym BaseIntegerType
annotation, SymExpr sym BaseIntegerType
annotatedBlkInt) <- sym
-> SymExpr sym BaseIntegerType
-> IO
     (SymAnnotation sym BaseIntegerType, SymExpr sym BaseIntegerType)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymExpr sym tp -> IO (SymAnnotation sym tp, SymExpr sym tp)
forall (tp :: BaseType).
sym -> SymExpr sym tp -> IO (SymAnnotation sym tp, SymExpr sym tp)
annotateTerm sym
sym (SymExpr sym BaseIntegerType
 -> IO
      (SymAnnotation sym BaseIntegerType, SymExpr sym BaseIntegerType))
-> IO (SymExpr sym BaseIntegerType)
-> IO
     (SymAnnotation sym BaseIntegerType, SymExpr sym BaseIntegerType)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymNat sym -> IO (SymExpr sym BaseIntegerType)
forall sym.
IsExprBuilder sym =>
sym -> SymNat sym -> IO (SymInteger sym)
natToInteger sym
sym SymNat sym
blk
     SymNat sym
annotatedBlkNat <- sym -> SymExpr sym BaseIntegerType -> IO (SymNat sym)
forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> IO (SymNat sym)
integerToNat sym
sym SymExpr sym BaseIntegerType
annotatedBlkInt
     (SymAnnotation sym BaseIntegerType, LLVMPointer sym w)
-> IO (SymAnnotation sym BaseIntegerType, LLVMPointer sym w)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SymAnnotation sym BaseIntegerType
annotation, SymNat sym -> SymBV sym w -> LLVMPointer sym w
forall sym (w :: Nat).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
LLVMPointer SymNat sym
annotatedBlkNat SymBV sym w
off)

annotatePointerOffset ::
  forall sym w. (IsSymInterface sym) =>
  sym ->
  LLVMPtr sym w ->
  IO (SymAnnotation sym (BaseBVType w), LLVMPointer sym w)
annotatePointerOffset :: forall sym (w :: Nat).
IsSymInterface sym =>
sym
-> LLVMPtr sym w
-> IO (SymAnnotation sym (BaseBVType w), LLVMPointer sym w)
annotatePointerOffset sym
sym (LLVMPointer SymNat sym
blk SymBV sym w
off) =
  do (SymAnnotation sym (BaseBVType w)
annotation, SymBV sym w
annotatedOff) <- sym
-> SymBV sym w
-> IO (SymAnnotation sym (BaseBVType w), SymBV sym w)
forall sym (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymExpr sym tp -> IO (SymAnnotation sym tp, SymExpr sym tp)
forall (tp :: BaseType).
sym -> SymExpr sym tp -> IO (SymAnnotation sym tp, SymExpr sym tp)
annotateTerm sym
sym SymBV sym w
off
     (SymAnnotation sym (BaseBVType w), LLVMPointer sym w)
-> IO (SymAnnotation sym (BaseBVType w), LLVMPointer sym w)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SymAnnotation sym (BaseBVType w)
annotation, SymNat sym -> SymBV sym w -> LLVMPointer sym w
forall sym (w :: Nat).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
LLVMPointer SymNat sym
blk SymBV sym w
annotatedOff)