------------------------------------------------------------------------ -- | -- 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 -- 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 (LLVMPointer blk _) = blk 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 =<< bvLit sym w (BV.zero w) 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 (LLVMPointer blk off) = do blk' <- integerToNat sym =<< intLit sym =<< conc =<< natToInteger sym blk off' <- concBV sym conc off pure (LLVMPointer blk' 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' sym conc (RV ptr) = RV <$> concPtr sym conc 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 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 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 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)