------------------------------------------------------------------------
-- |
-- 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 :: forall sym (w :: Nat). LLVMPtr sym w -> SymNat sym
llvmPointerBlock (LLVMPointer SymNat sym
blk SymBV sym w
_) = SymNat sym
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 :: 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 -> IO (SymExpr sym (BaseBVType w))
forall (w :: Nat) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
bvZero sym
sym NatRepr w
w

-- | A concrete LLVM pointer
data ConcLLVMPtr w
  = ConcLLVMPtr
    { -- | Concrete block number
      forall (w :: Nat). ConcLLVMPtr w -> Integer
concBlock :: Integer
      -- | Concrete offset
    , forall (w :: Nat). ConcLLVMPtr w -> BV w
concOffset :: BV.BV w
    , forall (w :: Nat). ConcLLVMPtr w -> NatRepr 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 :: forall sym (w :: Nat).
IsExprBuilder sym =>
(forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue sym (LLVMPointerType w) -> IO (ConcLLVMPtr w)
concLLVMPtr forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (LLVMPointer SymNat sym
blk SymBV sym w
off) =
  do Integer
concBlk <- SymExpr sym BaseIntegerType -> IO (GroundValue BaseIntegerType)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc (SymNat sym -> SymExpr sym BaseIntegerType
forall sym. SymNat sym -> SymInteger sym
natToIntegerPure SymNat sym
blk)
     BV w
concOff <- SymBV sym w -> IO (GroundValue (BaseBVType w))
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
conc SymBV sym w
off
     ConcLLVMPtr w -> IO (ConcLLVMPtr w)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Integer -> BV w -> NatRepr w -> ConcLLVMPtr w
forall (w :: Nat). Integer -> BV w -> NatRepr w -> ConcLLVMPtr w
ConcLLVMPtr Integer
concBlk BV w
concOff (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))

-- | Create a symbolic pointer from a concrete one
concLLVMPtrToSymbolic ::
  (IsExprBuilder sym, 1 <= w) =>
  sym ->
  ConcLLVMPtr w ->
  IO (RegValue sym (LLVMPointerType w))
concLLVMPtrToSymbolic :: forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> ConcLLVMPtr w -> IO (RegValue sym (LLVMPointerType w))
concLLVMPtrToSymbolic sym
sym (ConcLLVMPtr Integer
concBlk BV w
concOff NatRepr w
w) = do
  SymNat sym
symBlk <- 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
concBlk
  SymExpr sym (BaseBVType w)
symOff <- 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 BV w
concOff
  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 -> SymExpr sym (BaseBVType w) -> LLVMPointer sym w
forall sym (w :: Nat).
SymNat sym -> SymBV sym w -> LLVMPointer sym w
LLVMPointer SymNat sym
symBlk SymExpr sym (BaseBVType w)
symOff)

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 = sym
-> ConcLLVMPtr w
-> IO
     (RegValue
        sym (IntrinsicType "LLVM_pointer" (EmptyCtx '::> BVType w)))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> ConcLLVMPtr w -> IO (RegValue sym (LLVMPointerType w))
concLLVMPtrToSymbolic sym
sym (ConcLLVMPtr w -> IO (LLVMPointer sym w))
-> (LLVMPointer sym w -> IO (ConcLLVMPtr w))
-> LLVMPointer sym w
-> IO (LLVMPointer sym w)
forall (m :: Type -> Type) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue
     sym (IntrinsicType "LLVM_pointer" (EmptyCtx '::> BVType w))
-> IO (ConcLLVMPtr w)
forall sym (w :: Nat).
IsExprBuilder sym =>
(forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue sym (LLVMPointerType w) -> IO (ConcLLVMPtr w)
concLLVMPtr SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
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' :: 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

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

-- | An 'Conc.IntrinsicConcFn' for LLVM pointers
concPtrFn :: Conc.IntrinsicConcFn t "LLVM_pointer"
concPtrFn :: forall t. IntrinsicConcFn t "LLVM_pointer"
concPtrFn = (forall sym (ctx :: Ctx CrucibleType).
 (SymExpr sym ~ Expr t, IsExprBuilder sym) =>
 ConcCtx sym t
 -> Assignment TypeRepr ctx
 -> Intrinsic sym "LLVM_pointer" ctx
 -> IO (ConcRegValue sym (IntrinsicType "LLVM_pointer" ctx)))
-> IntrinsicConcFn t "LLVM_pointer"
forall t (nm :: Symbol).
(forall sym (ctx :: Ctx CrucibleType).
 (SymExpr sym ~ Expr t, IsExprBuilder sym) =>
 ConcCtx sym t
 -> Assignment TypeRepr ctx
 -> Intrinsic sym nm ctx
 -> IO (ConcRegValue sym (IntrinsicType nm ctx)))
-> IntrinsicConcFn t nm
Conc.IntrinsicConcFn ((forall sym (ctx :: Ctx CrucibleType).
  (SymExpr sym ~ Expr t, IsExprBuilder sym) =>
  ConcCtx sym t
  -> Assignment TypeRepr ctx
  -> Intrinsic sym "LLVM_pointer" ctx
  -> IO (ConcRegValue sym (IntrinsicType "LLVM_pointer" ctx)))
 -> IntrinsicConcFn t "LLVM_pointer")
-> (forall sym (ctx :: Ctx CrucibleType).
    (SymExpr sym ~ Expr t, IsExprBuilder sym) =>
    ConcCtx sym t
    -> Assignment TypeRepr ctx
    -> Intrinsic sym "LLVM_pointer" ctx
    -> IO (ConcRegValue sym (IntrinsicType "LLVM_pointer" ctx)))
-> IntrinsicConcFn t "LLVM_pointer"
forall a b. (a -> b) -> a -> b
$ \ConcCtx sym t
ctx Assignment TypeRepr ctx
tyCtx Intrinsic sym "LLVM_pointer" ctx
ptr ->
  case Assignment TypeRepr ctx -> AssignView TypeRepr ctx
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> AssignView f ctx
Ctx.viewAssign Assignment TypeRepr ctx
tyCtx of
    Ctx.AssignExtend (Assignment TypeRepr ctx1 -> AssignView TypeRepr ctx1
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> AssignView f ctx
Ctx.viewAssign -> AssignView TypeRepr ctx1
Ctx.AssignEmpty) (BVRepr NatRepr n
_) ->
      let W4GE.GroundEvalFn forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
ge = ConcCtx sym t -> GroundEvalFn t
forall sym t. ConcCtx sym t -> GroundEvalFn t
Conc.model ConcCtx sym t
ctx
      in (forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue sym (LLVMPointerType n) -> IO (ConcLLVMPtr n)
forall sym (w :: Nat).
IsExprBuilder sym =>
(forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp))
-> RegValue sym (LLVMPointerType w) -> IO (ConcLLVMPtr w)
concLLVMPtr Expr t tp -> IO (GroundValue tp)
SymExpr sym tp -> IO (GroundValue tp)
forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
forall (tp :: BaseType). SymExpr sym tp -> IO (GroundValue tp)
ge Intrinsic sym "LLVM_pointer" ctx
RegValue sym (LLVMPointerType n)
ptr
    -- These are impossible by the definition of LLVMPointerImpl
    AssignView TypeRepr ctx
Ctx.AssignEmpty ->
       String -> [String] -> IO (ConcIntrinsic "LLVM_pointer" EmptyCtx)
forall a. HasCallStack => String -> [String] -> a
panic String
"LLVM.MemModel.Pointer.concPtrFn"
         [ String
"Impossible: LLVMPointerType empty context" ]
    Ctx.AssignExtend Assignment TypeRepr ctx1
_ TypeRepr tp
_ ->
       String
-> [String] -> IO (ConcIntrinsic "LLVM_pointer" (ctx1 '::> tp))
forall a. HasCallStack => String -> [String] -> a
panic String
"LLVM.MemModel.Pointer.concPtrFn"
         [ String
"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 :: forall t. MapF SymbolRepr (IntrinsicConcFn t)
concPtrFnMap = SymbolRepr "LLVM_pointer"
-> IntrinsicConcFn t "LLVM_pointer"
-> MapF SymbolRepr (IntrinsicConcFn t)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
k tp -> a tp -> MapF k a
MapF.singleton (forall (s :: Symbol). KnownSymbol s => SymbolRepr s
knownSymbol @"LLVM_pointer") IntrinsicConcFn t "LLVM_pointer"
forall t. IntrinsicConcFn t "LLVM_pointer"
concPtrFn

-- | A 'Conc.IntrinsicConcToSymFn' for LLVM pointers
concToSymPtrFn :: Conc.IntrinsicConcToSymFn "LLVM_pointer"
concToSymPtrFn :: IntrinsicConcToSymFn "LLVM_pointer"
concToSymPtrFn = (forall sym (ctx :: Ctx CrucibleType).
 IsExprBuilder sym =>
 sym
 -> Assignment TypeRepr ctx
 -> ConcIntrinsic "LLVM_pointer" ctx
 -> IO (RegValue sym (IntrinsicType "LLVM_pointer" ctx)))
-> IntrinsicConcToSymFn "LLVM_pointer"
forall (nm :: Symbol).
(forall sym (ctx :: Ctx CrucibleType).
 IsExprBuilder sym =>
 sym
 -> Assignment TypeRepr ctx
 -> ConcIntrinsic nm ctx
 -> IO (RegValue sym (IntrinsicType nm ctx)))
-> IntrinsicConcToSymFn nm
Conc.IntrinsicConcToSymFn ((forall sym (ctx :: Ctx CrucibleType).
  IsExprBuilder sym =>
  sym
  -> Assignment TypeRepr ctx
  -> ConcIntrinsic "LLVM_pointer" ctx
  -> IO (RegValue sym (IntrinsicType "LLVM_pointer" ctx)))
 -> IntrinsicConcToSymFn "LLVM_pointer")
-> (forall sym (ctx :: Ctx CrucibleType).
    IsExprBuilder sym =>
    sym
    -> Assignment TypeRepr ctx
    -> ConcIntrinsic "LLVM_pointer" ctx
    -> IO (RegValue sym (IntrinsicType "LLVM_pointer" ctx)))
-> IntrinsicConcToSymFn "LLVM_pointer"
forall a b. (a -> b) -> a -> b
$ \sym
sym Assignment TypeRepr ctx
tyCtx ConcIntrinsic "LLVM_pointer" ctx
ptr ->
  case Assignment TypeRepr ctx -> AssignView TypeRepr ctx
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> AssignView f ctx
Ctx.viewAssign Assignment TypeRepr ctx
tyCtx of
    Ctx.AssignExtend (Assignment TypeRepr ctx1 -> AssignView TypeRepr ctx1
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> AssignView f ctx
Ctx.viewAssign -> AssignView TypeRepr ctx1
Ctx.AssignEmpty) (BVRepr NatRepr n
_) ->
      sym -> ConcLLVMPtr n -> IO (RegValue sym (LLVMPointerType n))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> ConcLLVMPtr w -> IO (RegValue sym (LLVMPointerType w))
concLLVMPtrToSymbolic sym
sym ConcIntrinsic "LLVM_pointer" ctx
ConcLLVMPtr n
ptr
    -- These are impossible by the definition of LLVMPointerImpl
    AssignView TypeRepr ctx
Ctx.AssignEmpty ->
       String -> [String] -> IO (TypeError ...)
forall a. HasCallStack => String -> [String] -> a
panic String
"LLVM.MemModel.Pointer.concToSymPtrFn"
         [ String
"Impossible: LLVMPointerType empty context" ]
    Ctx.AssignExtend Assignment TypeRepr ctx1
_ TypeRepr tp
_ ->
       String -> [String] -> IO (LLVMPointerImpl sym (ctx1 '::> tp))
forall a. HasCallStack => String -> [String] -> a
panic String
"LLVM.MemModel.Pointer.concToSymPtrFn"
         [ String
"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 SymbolRepr IntrinsicConcToSymFn
concToSymPtrFnMap = SymbolRepr "LLVM_pointer"
-> IntrinsicConcToSymFn "LLVM_pointer"
-> MapF SymbolRepr IntrinsicConcToSymFn
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
k tp -> a tp -> MapF k a
MapF.singleton (forall (s :: Symbol). KnownSymbol s => SymbolRepr s
knownSymbol @"LLVM_pointer") IntrinsicConcToSymFn "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 :: 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 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 :: forall (w :: Nat) sym.
(1 <= w, IsSymInterface sym) =>
sym -> LLVMPtr sym w -> LLVMPtr sym w -> IO (Pred sym)
ptrSameAlloc sym
sym (LLVMPointer SymNat sym
base1 SymBV sym w
_off1) (LLVMPointer SymNat sym
base2 SymBV sym w
_off2) =
  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

-- | 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 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 :: forall sym (w :: Nat).
IsSymInterface sym =>
sym -> LLVMPtr sym w -> IO (Pred sym)
ptrIsBv sym
sym (LLVMPointer SymNat sym
blk SymBV sym w
_off) =
  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
blk (SymNat sym -> IO (SymExpr sym BaseBoolType))
-> IO (SymNat sym) -> IO (SymExpr sym BaseBoolType)
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

-- | 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)