GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-29 17:17:05 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' of github.com:GaloisInc/macaw into HEAD

Browse Source
This commit is contained in:
Tristan Ravitch 2018-04-24 09:07:39 -07:00
commit bd686c3c2e
9 changed files with 196 additions and 208 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
.travis.yml
View File

@ -42,7 +42,7 @@ install:
script: script:
- travis_wait stack --no-terminal --skip-ghc-check setup - travis_wait stack --no-terminal --skip-ghc-check setup
- cd x86/tests - cd x86/tests
- stack build macaw-x86 - stack build macaw-x86 macaw-x86-symbolic
- stack test macaw-x86 - stack test macaw-x86
- cd ../.. - cd ../..
# - cabal check # - cabal check

1
base/src/Data/Macaw/AbsDomain/JumpBounds.hs
View File

@ -132,6 +132,7 @@ addUpperBound v u bnds
BVValue _ c | c <= u -> Right bnds BVValue _ c | c <= u -> Right bnds
| otherwise -> Left "Constant given upper bound that is statically less than given bounds" | otherwise -> Left "Constant given upper bound that is statically less than given bounds"
RelocatableValue{} -> Left "Relocatable value does not have upper bounds." RelocatableValue{} -> Left "Relocatable value does not have upper bounds."
SymbolValue{} -> Left "Symbol value does not have upper bounds."
AssignedValue a -> AssignedValue a ->
case assignRhs a of case assignRhs a of
EvalApp (UExt x _) -> addUpperBound x u bnds EvalApp (UExt x _) -> addUpperBound x u bnds

7
base/src/Data/Macaw/AbsDomain/Refine.hs
View File

@ -42,9 +42,10 @@ refineProcState :: RefineConstraints arch
-> AbsValue (ArchAddrWidth arch) tp -- ^ Abstract value to assign value. -> AbsValue (ArchAddrWidth arch) tp -- ^ Abstract value to assign value.
-> AbsProcessorState (ArchReg arch) ids -> AbsProcessorState (ArchReg arch) ids
-> AbsProcessorState (ArchReg arch) ids -> AbsProcessorState (ArchReg arch) ids
refineProcState (BoolValue _) _av regs = regs -- Skip refinment for literal values refineProcState (BoolValue _) _av regs = regs -- Skip refinement for literal values
refineProcState (BVValue _n _val) _av regs = regs -- Skip refinment for literal values refineProcState (BVValue _n _val) _av regs = regs -- Skip refinement for literal values
refineProcState (RelocatableValue _ _) _av regs = regs -- Skip refinment for relocatable values refineProcState (RelocatableValue _ _) _av regs = regs -- Skip refinement for relocatable values
refineProcState (SymbolValue _ _) _av regs = regs -- Skip refinement for this case.
refineProcState (Initial r) av regs = refineProcState (Initial r) av regs =
regs & (absInitialRegs . boundValue r) %~ flip meet av regs & (absInitialRegs . boundValue r) %~ flip meet av
refineProcState (AssignedValue (Assignment a_id rhs)) av regs refineProcState (AssignedValue (Assignment a_id rhs)) av regs

1
base/src/Data/Macaw/CFG/Rewriter.hs
View File

@ -30,7 +30,6 @@ import Data.Parameterized.Map (MapF)
import qualified Data.Parameterized.Map as MapF import qualified Data.Parameterized.Map as MapF
import Data.Parameterized.NatRepr import Data.Parameterized.NatRepr
import Data.Parameterized.Nonce import Data.Parameterized.Nonce
import Data.Parameterized.Some
import Data.Parameterized.TraversableFC import Data.Parameterized.TraversableFC
import Data.STRef import Data.STRef

12
base/src/Data/Macaw/Memory.hs
View File

@ -144,6 +144,7 @@ import GHC.TypeLits
import Numeric (showHex) import Numeric (showHex)
import Text.PrettyPrint.ANSI.Leijen hiding ((<$>), (<>)) import Text.PrettyPrint.ANSI.Leijen hiding ((<$>), (<>))
import Data.Parameterized.Classes
import Data.Parameterized.NatRepr import Data.Parameterized.NatRepr
import qualified Data.Macaw.Memory.Permissions as Perm import qualified Data.Macaw.Memory.Permissions as Perm
@ -158,6 +159,17 @@ data AddrWidthRepr w
| (w ~ 64) => Addr64 | (w ~ 64) => Addr64
-- ^ A 64-bit address -- ^ A 64-bit address
instance TestEquality AddrWidthRepr where
testEquality Addr32 Addr32 = Just Refl
testEquality Addr64 Addr64 = Just Refl
testEquality _ _ = Nothing
instance OrdF AddrWidthRepr where
compareF Addr32 Addr32 = EQF
compareF Addr32 Addr64 = LTF
compareF Addr64 Addr32 = GTF
compareF Addr64 Addr64 = EQF
-- | The nat representation of this address. -- | The nat representation of this address.
addrWidthNatRepr :: AddrWidthRepr w -> NatRepr w addrWidthNatRepr :: AddrWidthRepr w -> NatRepr w
addrWidthNatRepr Addr32 = knownNat addrWidthNatRepr Addr32 = knownNat

10
symbolic/src/Data/Macaw/Symbolic.hs
View File

@ -47,8 +47,8 @@ import Data.Foldable
import Data.Map.Strict (Map) import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map import qualified Data.Map.Strict as Map
import Data.Parameterized.Context as Ctx import Data.Parameterized.Context as Ctx
import qualified Data.Set as Set --import qualified Data.Set as Set
import qualified Data.Text as Text --import qualified Data.Text as Text
import Data.Word import Data.Word
import qualified Lang.Crucible.Analysis.Postdom as C import qualified Lang.Crucible.Analysis.Postdom as C
import qualified Lang.Crucible.CFG.Core as C import qualified Lang.Crucible.CFG.Core as C
@ -82,6 +82,7 @@ import Data.Macaw.Symbolic.MemOps
data MacawSimulatorState sym = MacawSimulatorState data MacawSimulatorState sym = MacawSimulatorState
{-
mkMemSegmentBinding :: (1 <= w) mkMemSegmentBinding :: (1 <= w)
=> C.HandleAllocator s => C.HandleAllocator s
-> NatRepr w -> NatRepr w
@ -103,6 +104,7 @@ mkMemBaseVarMap halloc mem = do
, M.segmentBase seg /= 0 , M.segmentBase seg /= 0
] ]
Map.fromList <$> traverse (mkMemSegmentBinding halloc (M.memWidth mem)) (Set.toList baseIndices) Map.fromList <$> traverse (mkMemSegmentBinding halloc (M.memWidth mem)) (Set.toList baseIndices)
-}
-- | Create a Crucible CFG from a list of blocks -- | Create a Crucible CFG from a list of blocks
mkCrucCFG :: forall s arch ids mkCrucCFG :: forall s arch ids
@ -290,7 +292,7 @@ evalMacawExprExtension sym _iTypes _logFn f e0 =
PtrToBits w x -> doPtrToBits sym w =<< f x PtrToBits w x -> doPtrToBits sym w =<< f x
BitsToPtr _w x -> MM.llvmPointer_bv sym =<< f x BitsToPtr _w x -> MM.llvmPointer_bv sym =<< f x
MacawNullPtr w | LeqProof <- lemma1_16 w -> MM.mkNullPointer sym w MacawNullPtr w | LeqProof <- addrWidthIsPos w -> MM.mkNullPointer sym (M.addrWidthNatRepr w)
type EvalStmtFunc f p sym ext = type EvalStmtFunc f p sym ext =
forall rtp blocks r ctx tp'. forall rtp blocks r ctx tp'.
@ -321,7 +323,7 @@ execMacawStmtExtension archStmtFn mvar globs callH s0 st =
MacawCondReadMem w mr p x d -> doCondReadMem st mvar globs w mr p x d MacawCondReadMem w mr p x d -> doCondReadMem st mvar globs w mr p x d
MacawWriteMem w mr x v -> doWriteMem st mvar globs w mr x v MacawWriteMem w mr x v -> doWriteMem st mvar globs w mr x v
MacawGlobalPtr addr -> doGetGlobal st mvar globs addr MacawGlobalPtr w addr -> M.addrWidthClass w $ doGetGlobal st mvar globs addr
MacawFreshSymbolic t -> -- XXX: user freshValue MacawFreshSymbolic t -> -- XXX: user freshValue
do nm <- case userSymbol "macawFresh" of do nm <- case userSymbol "macawFresh" of

234
symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
View File

@ -47,18 +47,18 @@ module Data.Macaw.Symbolic.CrucGen
, valueToCrucible , valueToCrucible
, evalArchStmt , evalArchStmt
, MemSegmentMap , MemSegmentMap
, lemma1_16
-- * Additional exports -- * Additional exports
, runCrucGen , runCrucGen
, setMachineRegs , setMachineRegs
, addTermStmt , addTermStmt
, parsedBlockLabel , parsedBlockLabel
, ArchAddrWidthRepr
, addrWidthIsPos
) where ) where
import Control.Lens hiding (Empty, (:>)) import Control.Lens hiding (Empty, (:>))
import Control.Monad.Except import Control.Monad.Except
import Control.Monad.ST import Control.Monad.ST
import GHC.TypeLits(KnownNat)
import Control.Monad.State.Strict import Control.Monad.State.Strict
import Data.Bits import Data.Bits
import qualified Data.Macaw.CFG as M import qualified Data.Macaw.CFG as M
@ -76,6 +76,7 @@ import qualified Data.Parameterized.Map as MapF
import Data.Parameterized.TraversableF import Data.Parameterized.TraversableF
import Data.Parameterized.TraversableFC import Data.Parameterized.TraversableFC
import qualified Data.Parameterized.TH.GADT as U import qualified Data.Parameterized.TH.GADT as U
import Data.Proxy
import qualified Data.Sequence as Seq import qualified Data.Sequence as Seq
@ -105,6 +106,8 @@ type ArchAddrCrucibleType arch = MM.LLVMPointerType (M.ArchAddrWidth arch)
type MacawFunctionArgs arch = EmptyCtx ::> ArchRegStruct arch type MacawFunctionArgs arch = EmptyCtx ::> ArchRegStruct arch
type MacawFunctionResult arch = ArchRegStruct arch type MacawFunctionResult arch = ArchRegStruct arch
type ArchAddrWidthRepr arch = M.AddrWidthRepr (M.ArchAddrWidth arch)
type family MacawArchStmtExtension (arch :: *) :: (C.CrucibleType -> *) -> C.CrucibleType -> * type family MacawArchStmtExtension (arch :: *) :: (C.CrucibleType -> *) -> C.CrucibleType -> *
type MacawArchConstraints arch = type MacawArchConstraints arch =
@ -113,14 +116,11 @@ type MacawArchConstraints arch =
, C.PrettyApp (MacawArchStmtExtension arch) , C.PrettyApp (MacawArchStmtExtension arch)
, M.MemWidth (M.RegAddrWidth (M.ArchReg arch)) , M.MemWidth (M.RegAddrWidth (M.ArchReg arch))
, M.PrettyF (M.ArchReg arch) , M.PrettyF (M.ArchReg arch)
, KnownNat (M.ArchAddrWidth arch)
, 16 <= M.ArchAddrWidth arch
) )
------------------------------------------------------------------------ ------------------------------------------------------------------------
-- CrucPersistentState -- CrucPersistentState
-- | Architecture-specific information needed to translate from Macaw to Crucible -- | Architecture-specific information needed to translate from Macaw to Crucible
data MacawSymbolicArchFunctions arch data MacawSymbolicArchFunctions arch
= MacawSymbolicArchFunctions = MacawSymbolicArchFunctions
@ -144,6 +144,10 @@ data MacawSymbolicArchFunctions arch
-- ^ Generate crucible for architecture-specific terminal statement. -- ^ Generate crucible for architecture-specific terminal statement.
} }
crucGenAddrWidth :: MacawSymbolicArchFunctions arch -> ArchAddrWidthRepr arch
crucGenAddrWidth fns =
crucGenArchConstraints fns $ M.addrWidthRepr Proxy
-- | Return types of registers in Crucible -- | Return types of registers in Crucible
crucArchRegTypes :: crucArchRegTypes ::
MacawSymbolicArchFunctions arch -> MacawSymbolicArchFunctions arch ->
@ -167,8 +171,7 @@ type ArchNatRepr a = NatRepr (M.ArchAddrWidth a)
data MacawExprExtension (arch :: *) data MacawExprExtension (arch :: *)
(f :: C.CrucibleType -> *) (f :: C.CrucibleType -> *)
(tp :: C.CrucibleType) (tp :: C.CrucibleType) where
where
MacawOverflows :: (1 <= w) MacawOverflows :: (1 <= w)
=> !MacawOverflowOp => !MacawOverflowOp
-> !(NatRepr w) -> !(NatRepr w)
@ -178,11 +181,11 @@ data MacawExprExtension (arch :: *)
-> MacawExprExtension arch f C.BoolType -> MacawExprExtension arch f C.BoolType
-- | Treat a pointer as a number. -- | Treat a pointer as a number.
PtrToBits :: PtrToBits
(1 <= w) => :: (1 <= w)
!(NatRepr w) -> => !(NatRepr w)
!(f (MM.LLVMPointerType w)) -> -> !(f (MM.LLVMPointerType w))
MacawExprExtension arch f (C.BVType w) -> MacawExprExtension arch f (C.BVType w)
-- | Treat a number as a pointer. -- | Treat a number as a pointer.
-- We can never read from this pointer. -- We can never read from this pointer.
@ -193,11 +196,9 @@ data MacawExprExtension (arch :: *)
MacawExprExtension arch f (MM.LLVMPointerType w) MacawExprExtension arch f (MM.LLVMPointerType w)
-- | A null pointer. -- | A null pointer.
MacawNullPtr :: MacawNullPtr
(16 <= M.ArchAddrWidth arch) => :: !(ArchAddrWidthRepr arch)
!(ArchNatRepr arch) -> -> MacawExprExtension arch f (BVPtr arch)
MacawExprExtension arch f (BVPtr arch)
instance C.PrettyApp (MacawExprExtension arch) where instance C.PrettyApp (MacawExprExtension arch) where
ppApp f a0 = ppApp f a0 =
@ -211,13 +212,17 @@ instance C.PrettyApp (MacawExprExtension arch) where
MacawNullPtr _ -> sexpr "null_ptr" [] MacawNullPtr _ -> sexpr "null_ptr" []
addrWidthIsPos :: M.AddrWidthRepr w -> LeqProof 1 w
addrWidthIsPos M.Addr32 = LeqProof
addrWidthIsPos M.Addr64 = LeqProof
instance C.TypeApp (MacawExprExtension arch) where instance C.TypeApp (MacawExprExtension arch) where
appType x = appType x =
case x of case x of
MacawOverflows {} -> C.knownRepr MacawOverflows {} -> C.knownRepr
PtrToBits w _ -> C.BVRepr w PtrToBits w _ -> C.BVRepr w
BitsToPtr w _ -> MM.LLVMPointerRepr w BitsToPtr w _ -> MM.LLVMPointerRepr w
MacawNullPtr w | LeqProof <- lemma1_16 w -> MM.LLVMPointerRepr w MacawNullPtr w | LeqProof <- addrWidthIsPos w -> MM.LLVMPointerRepr (M.addrWidthNatRepr w)
------------------------------------------------------------------------ ------------------------------------------------------------------------
@ -230,9 +235,7 @@ data MacawStmtExtension (arch :: *)
-- | Read from memory. -- | Read from memory.
MacawReadMem :: MacawReadMem ::
(16 <= M.ArchAddrWidth arch) => !(ArchAddrWidthRepr arch) ->
!(ArchNatRepr arch) ->
-- Info about memory (endianness, size) -- Info about memory (endianness, size)
!(M.MemRepr tp) -> !(M.MemRepr tp) ->
@ -245,44 +248,37 @@ data MacawStmtExtension (arch :: *)
-- | Read from memory, if the condition is True. -- | Read from memory, if the condition is True.
-- Otherwise, just return the given value. -- Otherwise, just return the given value.
MacawCondReadMem :: MacawCondReadMem
(16 <= M.ArchAddrWidth arch) => :: !(ArchAddrWidthRepr arch)
!(ArchNatRepr arch) ->
-- Info about memory (endianness, size) -- Info about memory (endianness, size)
!(M.MemRepr tp) -> -> !(M.MemRepr tp)
-- Condition -- Condition
!(f C.BoolType) -> -> !(f C.BoolType)
-- Pointer to read from -- Pointer to read from
!(f (ArchAddrCrucibleType arch)) -> -> !(f (ArchAddrCrucibleType arch))
-- Default value, returned if the condition is False. -- Default value, returned if the condition is False.
!(f (ToCrucibleType tp)) -> -> !(f (ToCrucibleType tp))
-> MacawStmtExtension arch f (ToCrucibleType tp)
MacawStmtExtension arch f (ToCrucibleType tp)
-- | Write to memory -- | Write to memory
MacawWriteMem :: MacawWriteMem
(16 <= M.ArchAddrWidth arch) => :: !(ArchAddrWidthRepr arch)
!(ArchNatRepr arch) -> -> !(M.MemRepr tp)
!(M.MemRepr tp) -> -> !(f (ArchAddrCrucibleType arch))
!(f (ArchAddrCrucibleType arch)) -> -> !(f (ToCrucibleType tp))
!(f (ToCrucibleType tp)) -> -> MacawStmtExtension arch f C.UnitType
MacawStmtExtension arch f C.UnitType
-- | Get the pointer associated with the given global address. -- | Get the pointer associated with the given global address.
MacawGlobalPtr :: MacawGlobalPtr
(16 <= M.ArchAddrWidth arch, M.MemWidth (M.ArchAddrWidth arch)) => :: !(ArchAddrWidthRepr arch)
!(M.MemAddr (M.ArchAddrWidth arch)) -> -> !(M.MemAddr (M.ArchAddrWidth arch))
MacawStmtExtension arch f (BVPtr arch) -> MacawStmtExtension arch f (BVPtr arch)
-- | Generate a fresh symbolic variable of the given type. -- | Generate a fresh symbolic variable of the given type.
MacawFreshSymbolic :: MacawFreshSymbolic
!(M.TypeRepr tp) -> MacawStmtExtension arch f (ToCrucibleType tp) :: !(M.TypeRepr tp)
-> MacawStmtExtension arch f (ToCrucibleType tp)
-- | Call a function. -- | Call a function.
MacawCall :: MacawCall ::
@ -310,32 +306,28 @@ data MacawStmtExtension (arch :: *)
-- | Equality for pointer or bit-vector. -- | Equality for pointer or bit-vector.
PtrEq :: PtrEq ::
(16 <= M.ArchAddrWidth arch) => !(ArchAddrWidthRepr arch) ->
!(ArchNatRepr arch) ->
!(f (BVPtr arch)) -> !(f (BVPtr arch)) ->
!(f (BVPtr arch)) -> !(f (BVPtr arch)) ->
MacawStmtExtension arch f C.BoolType MacawStmtExtension arch f C.BoolType
-- | Unsigned comparison for pointer/bit-vector. -- | Unsigned comparison for pointer/bit-vector.
PtrLeq :: PtrLeq ::
(16 <= M.ArchAddrWidth arch) => !(ArchAddrWidthRepr arch) ->
!(ArchNatRepr arch) ->
!(f (BVPtr arch)) -> !(f (BVPtr arch)) ->
!(f (BVPtr arch)) -> !(f (BVPtr arch)) ->
MacawStmtExtension arch f C.BoolType MacawStmtExtension arch f C.BoolType
-- | Unsigned comparison for pointer/bit-vector. -- | Unsigned comparison for pointer/bit-vector.
PtrLt :: PtrLt ::
(16 <= M.ArchAddrWidth arch) => !(ArchAddrWidthRepr arch) ->
!(ArchNatRepr arch) ->
!(f (BVPtr arch)) -> !(f (BVPtr arch)) ->
!(f (BVPtr arch)) -> !(f (BVPtr arch)) ->
MacawStmtExtension arch f C.BoolType MacawStmtExtension arch f C.BoolType
-- | Mux for pointers or bit-vectors. -- | Mux for pointers or bit-vectors.
PtrMux :: PtrMux ::
(16 <= M.ArchAddrWidth arch) => !(ArchAddrWidthRepr arch) ->
!(ArchNatRepr arch) ->
!(f C.BoolType) -> !(f C.BoolType) ->
!(f (BVPtr arch)) -> !(f (BVPtr arch)) ->
!(f (BVPtr arch)) -> !(f (BVPtr arch)) ->
@ -343,16 +335,14 @@ data MacawStmtExtension (arch :: *)
-- | Add a pointer to a bit-vector, or two bit-vectors. -- | Add a pointer to a bit-vector, or two bit-vectors.
PtrAdd :: PtrAdd ::
(16 <= M.ArchAddrWidth arch) => !(ArchAddrWidthRepr arch) ->
!(ArchNatRepr arch) ->
!(f (BVPtr arch)) -> !(f (BVPtr arch)) ->
!(f (BVPtr arch)) -> !(f (BVPtr arch)) ->
MacawStmtExtension arch f (BVPtr arch) MacawStmtExtension arch f (BVPtr arch)
-- | Subtract two pointers, two bit-vectors, or bit-vector from a pointer. -- | Subtract two pointers, two bit-vectors, or bit-vector from a pointer.
PtrSub :: PtrSub ::
(16 <= M.ArchAddrWidth arch) => !(ArchAddrWidthRepr arch) ->
!(ArchNatRepr arch) ->
!(f (BVPtr arch)) -> !(f (BVPtr arch)) ->
!(f (BVPtr arch)) -> !(f (BVPtr arch)) ->
MacawStmtExtension arch f (BVPtr arch) MacawStmtExtension arch f (BVPtr arch)
@ -361,8 +351,7 @@ data MacawStmtExtension (arch :: *)
-- but sometimes we need to support "and"-ing a pointer with a constant, -- but sometimes we need to support "and"-ing a pointer with a constant,
-- which happens when trying to align a pointer. -- which happens when trying to align a pointer.
PtrAnd :: PtrAnd ::
(16 <= M.ArchAddrWidth arch) => !(ArchAddrWidthRepr arch) ->
!(ArchNatRepr arch) ->
!(f (BVPtr arch)) -> !(f (BVPtr arch)) ->
!(f (BVPtr arch)) -> !(f (BVPtr arch)) ->
MacawStmtExtension arch f (BVPtr arch) MacawStmtExtension arch f (BVPtr arch)
@ -391,7 +380,7 @@ instance (C.PrettyApp (MacawArchStmtExtension arch),
MacawReadMem _ r a -> sexpr "macawReadMem" [pretty r, f a] MacawReadMem _ r a -> sexpr "macawReadMem" [pretty r, f a]
MacawCondReadMem _ r c a d -> sexpr "macawCondReadMem" [pretty r, f c, f a, f d ] MacawCondReadMem _ r c a d -> sexpr "macawCondReadMem" [pretty r, f c, f a, f d ]
MacawWriteMem _ r a v -> sexpr "macawWriteMem" [pretty r, f a, f v] MacawWriteMem _ r a v -> sexpr "macawWriteMem" [pretty r, f a, f v]
MacawGlobalPtr x -> sexpr "global" [ text (show x) ] MacawGlobalPtr _ x -> sexpr "global" [ text (show x) ]
MacawFreshSymbolic r -> sexpr "macawFreshSymbolic" [ text (show r) ] MacawFreshSymbolic r -> sexpr "macawFreshSymbolic" [ text (show r) ]
MacawCall _ regs -> sexpr "macawCall" [ f regs ] MacawCall _ regs -> sexpr "macawCall" [ f regs ]
@ -416,9 +405,8 @@ instance C.TypeApp (MacawArchStmtExtension arch)
appType (MacawReadMem _ r _) = memReprToCrucible r appType (MacawReadMem _ r _) = memReprToCrucible r
appType (MacawCondReadMem _ r _ _ _) = memReprToCrucible r appType (MacawCondReadMem _ r _ _ _) = memReprToCrucible r
appType (MacawWriteMem _ _ _ _) = C.knownRepr appType (MacawWriteMem _ _ _ _) = C.knownRepr
appType (MacawGlobalPtr a) appType (MacawGlobalPtr w _)
| let w = M.addrWidthNatRepr (M.addrWidthRepr a) | LeqProof <- addrWidthIsPos w = MM.LLVMPointerRepr (M.addrWidthNatRepr w)
, LeqProof <- lemma1_16 w = MM.LLVMPointerRepr w
appType (MacawFreshSymbolic r) = typeToCrucible r appType (MacawFreshSymbolic r) = typeToCrucible r
appType (MacawCall regTypes _) = C.StructRepr regTypes appType (MacawCall regTypes _) = C.StructRepr regTypes
appType (MacawArchStmtExtension f) = C.appType f appType (MacawArchStmtExtension f) = C.appType f
@ -426,16 +414,10 @@ instance C.TypeApp (MacawArchStmtExtension arch)
appType PtrEq {} = C.knownRepr appType PtrEq {} = C.knownRepr
appType PtrLt {} = C.knownRepr appType PtrLt {} = C.knownRepr
appType PtrLeq {} = C.knownRepr appType PtrLeq {} = C.knownRepr
appType (PtrAdd w _ _) | LeqProof <- lemma1_16 w = MM.LLVMPointerRepr w appType (PtrAdd w _ _) | LeqProof <- addrWidthIsPos w = MM.LLVMPointerRepr (M.addrWidthNatRepr w)
appType (PtrAnd w _ _) | LeqProof <- lemma1_16 w = MM.LLVMPointerRepr w appType (PtrAnd w _ _) | LeqProof <- addrWidthIsPos w = MM.LLVMPointerRepr (M.addrWidthNatRepr w)
appType (PtrSub w _ _) | LeqProof <- lemma1_16 w = MM.LLVMPointerRepr w appType (PtrSub w _ _) | LeqProof <- addrWidthIsPos w = MM.LLVMPointerRepr (M.addrWidthNatRepr w)
appType (PtrMux w _ _ _) | LeqProof <- lemma1_16 w = MM.LLVMPointerRepr w appType (PtrMux w _ _ _) | LeqProof <- addrWidthIsPos w = MM.LLVMPointerRepr (M.addrWidthNatRepr w)
lemma1_16 :: (16 <= w) => p w -> LeqProof 1 w
lemma1_16 w = leqTrans p (leqProof knownNat w)
where
p :: LeqProof 1 16
p = leqProof knownNat knownNat
------------------------------------------------------------------------ ------------------------------------------------------------------------
-- MacawExt -- MacawExt
@ -514,10 +496,8 @@ instance MonadState (CrucGenState arch ids s) (CrucGen arch ids s) where
put s = CrucGen $ \_ cont -> cont s () put s = CrucGen $ \_ cont -> cont s ()
-- | A NatRepr corresponding to the architecture width. -- | A NatRepr corresponding to the architecture width.
archAddrWidth :: CrucGen arch ids s (NatRepr (M.ArchAddrWidth arch)) archAddrWidth :: CrucGen arch ids s (ArchAddrWidthRepr arch)
archAddrWidth = archAddrWidth = crucGenAddrWidth . translateFns <$> get
do archFns <- translateFns <$> get
crucGenArchConstraints archFns (return knownRepr)
-- | Get current position -- | Get current position
getPos :: CrucGen arch ids s C.Position getPos :: CrucGen arch ids s C.Position
@ -676,8 +656,8 @@ appToCrucible app = do
M.BoolTypeRepr -> appAtom (C.BaseIsEq C.BaseBoolRepr xv yv) M.BoolTypeRepr -> appAtom (C.BaseIsEq C.BaseBoolRepr xv yv)
M.BVTypeRepr n -> M.BVTypeRepr n ->
do rW <- archAddrWidth do rW <- archAddrWidth
case testEquality n rW of case testEquality n (M.addrWidthNatRepr rW) of
Just Refl -> evalMacawStmt (PtrEq n xv yv) Just Refl -> evalMacawStmt (PtrEq rW xv yv)
Nothing -> Nothing ->
appAtom =<< C.BVEq n <$> toBits n xv <*> toBits n yv appAtom =<< C.BVEq n <$> toBits n xv <*> toBits n yv
M.TupleTypeRepr _ -> fail "XXX: Equality on tuples not yet done." M.TupleTypeRepr _ -> fail "XXX: Equality on tuples not yet done."
@ -691,8 +671,8 @@ appToCrucible app = do
M.BoolTypeRepr -> appAtom (C.BaseIte C.BaseBoolRepr cond tv fv) M.BoolTypeRepr -> appAtom (C.BaseIte C.BaseBoolRepr cond tv fv)
M.BVTypeRepr n -> M.BVTypeRepr n ->
do rW <- archAddrWidth do rW <- archAddrWidth
case testEquality n rW of case testEquality n (M.addrWidthNatRepr rW) of
Just Refl -> evalMacawStmt (PtrMux n cond tv fv) Just Refl -> evalMacawStmt (PtrMux rW cond tv fv)
Nothing -> appBVAtom n =<< Nothing -> appBVAtom n =<<
C.BVIte cond n <$> toBits n tv <*> toBits n fv C.BVIte cond n <$> toBits n tv <*> toBits n fv
M.TupleTypeRepr _ -> fail "XXX: Mux on tuples not yet done." M.TupleTypeRepr _ -> fail "XXX: Mux on tuples not yet done."
@ -728,8 +708,8 @@ appToCrucible app = do
do xv <- v2c x do xv <- v2c x
yv <- v2c y yv <- v2c y
aw <- archAddrWidth aw <- archAddrWidth
case testEquality w aw of case testEquality w (M.addrWidthNatRepr aw) of
Just Refl -> evalMacawStmt (PtrAdd w xv yv) Just Refl -> evalMacawStmt (PtrAdd aw xv yv)
Nothing -> appBVAtom w =<< C.BVAdd w <$> toBits w xv <*> toBits w yv Nothing -> appBVAtom w =<< C.BVAdd w <$> toBits w xv <*> toBits w yv
-- Here we assume that this does not make sense for pointers. -- Here we assume that this does not make sense for pointers.
@ -744,8 +724,8 @@ appToCrucible app = do
do xv <- v2c x do xv <- v2c x
yv <- v2c y yv <- v2c y
aw <- archAddrWidth aw <- archAddrWidth
case testEquality w aw of case testEquality w (M.addrWidthNatRepr aw) of
Just Refl -> evalMacawStmt (PtrSub w xv yv) Just Refl -> evalMacawStmt (PtrSub aw xv yv)
Nothing -> appBVAtom w =<< C.BVSub w <$> toBits w xv <*> toBits w yv Nothing -> appBVAtom w =<< C.BVSub w <$> toBits w xv <*> toBits w yv
M.BVSbb w x y c -> do M.BVSbb w x y c -> do
@ -758,23 +738,23 @@ appToCrucible app = do
M.BVMul w x y -> bitOp2 w (C.BVMul w) x y M.BVMul w x y -> bitOp2 w (C.BVMul w) x y
M.BVUnsignedLe x y -> M.BVUnsignedLe x y -> do
do let w = M.typeWidth x let w = M.typeWidth x
ptrW <- archAddrWidth ptrW <- archAddrWidth
xv <- v2c x xv <- v2c x
yv <- v2c y yv <- v2c y
case testEquality w ptrW of case testEquality w (M.addrWidthNatRepr ptrW) of
Just Refl -> evalMacawStmt (PtrLeq w xv yv) Just Refl -> evalMacawStmt (PtrLeq ptrW xv yv)
Nothing -> appAtom =<< C.BVUle w <$> toBits w xv <*> toBits w yv Nothing -> appAtom =<< C.BVUle w <$> toBits w xv <*> toBits w yv
M.BVUnsignedLt x y -> M.BVUnsignedLt x y -> do
do let w = M.typeWidth x let w = M.typeWidth x
ptrW <- archAddrWidth ptrW <- archAddrWidth
xv <- v2c x xv <- v2c x
yv <- v2c y yv <- v2c y
case testEquality w ptrW of case testEquality w (M.addrWidthNatRepr ptrW) of
Just Refl -> evalMacawStmt (PtrLt w xv yv) Just Refl -> evalMacawStmt (PtrLt ptrW xv yv)
Nothing -> appAtom =<< C.BVUlt w <$> toBits w xv <*> toBits w yv Nothing -> appAtom =<< C.BVUlt w <$> toBits w xv <*> toBits w yv
M.BVSignedLe x y -> M.BVSignedLe x y ->
do let w = M.typeWidth x do let w = M.typeWidth x
@ -797,13 +777,13 @@ appToCrucible app = do
M.BVComplement w x -> appBVAtom w =<< C.BVNot w <$> v2c' w x M.BVComplement w x -> appBVAtom w =<< C.BVNot w <$> v2c' w x
M.BVAnd w x y -> M.BVAnd w x y -> do
do xv <- v2c x xv <- v2c x
yv <- v2c y yv <- v2c y
aw <- archAddrWidth aw <- archAddrWidth
case testEquality w aw of case testEquality w (M.addrWidthNatRepr aw) of
Just Refl -> evalMacawStmt (PtrAnd w xv yv) Just Refl -> evalMacawStmt (PtrAnd aw xv yv)
Nothing -> appBVAtom w =<< C.BVAnd w <$> toBits w xv <*> toBits w yv Nothing -> appBVAtom w =<< C.BVAnd w <$> toBits w xv <*> toBits w yv
M.BVOr w x y -> bitOp2 w (C.BVOr w) x y M.BVOr w x y -> bitOp2 w (C.BVOr w) x y
M.BVXor w x y -> bitOp2 w (C.BVXor w) x y M.BVXor w x y -> bitOp2 w (C.BVXor w) x y
@ -836,8 +816,6 @@ appToCrucible app = do
M.Bsr w x -> do M.Bsr w x -> do
undefined w x undefined w x
valueToCrucible :: M.Value arch ids tp valueToCrucible :: M.Value arch ids tp
-> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp)) -> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp))
valueToCrucible v = do valueToCrucible v = do
@ -847,20 +825,12 @@ valueToCrucible v = do
M.BVValue w c -> fromBits w =<< bvLit w c M.BVValue w c -> fromBits w =<< bvLit w c
M.BoolValue b -> crucibleValue (C.BoolLit b) M.BoolValue b -> crucibleValue (C.BoolLit b)
M.RelocatableValue w addr -> M.RelocatableValue w addr
do rW <- archAddrWidth | M.addrBase addr == 0 && M.addrOffset addr == 0 ->
case testEquality w rW of evalMacawExt (MacawNullPtr w)
Just Refl | otherwise -> evalMacawStmt (MacawGlobalPtr w addr)
| M.addrBase addr == 0 && M.addrOffset addr == 0 -> M.SymbolValue{} -> do
evalMacawExt (MacawNullPtr w) error "macaw-symbolic does not yet support symbol values."
| otherwise -> evalMacawStmt (MacawGlobalPtr addr)
Nothing ->
fail $ unlines [ "Unexpected relocatable value width"
, "*** Expected: " ++ show rW
, "*** Width: " ++ show w
, "*** Base: " ++ show (M.addrBase addr)
, "*** Offset: " ++ show (M.addrOffset addr)
]
M.Initial r -> M.Initial r ->
getRegValue r getRegValue r
@ -1207,7 +1177,7 @@ instance TestEqualityFC (MacawExprExtension arch) where
$(U.structuralTypeEquality [t|MacawExprExtension|] $(U.structuralTypeEquality [t|MacawExprExtension|]
[ (U.DataArg 1 `U.TypeApp` U.AnyType, [|f|]) [ (U.DataArg 1 `U.TypeApp` U.AnyType, [|f|])
, (U.ConType [t|NatRepr |] `U.TypeApp` U.AnyType, [|testEquality|]) , (U.ConType [t|NatRepr |] `U.TypeApp` U.AnyType, [|testEquality|])
, (U.ConType [t|ArchAddrWidthRepr|] `U.TypeApp` U.AnyType, [|testEquality|])
]) ])
instance OrdFC (MacawExprExtension arch) where instance OrdFC (MacawExprExtension arch) where
@ -1216,7 +1186,7 @@ instance OrdFC (MacawExprExtension arch) where
[ (U.DataArg 1 `U.TypeApp` U.AnyType, [|f|]) [ (U.DataArg 1 `U.TypeApp` U.AnyType, [|f|])
, (U.ConType [t|NatRepr|] `U.TypeApp` U.AnyType, [|compareF|]) , (U.ConType [t|NatRepr|] `U.TypeApp` U.AnyType, [|compareF|])
, (U.ConType [t|ArchNatRepr|] `U.TypeApp` U.AnyType, [|compareF|]) , (U.ConType [t|ArchNatRepr|] `U.TypeApp` U.AnyType, [|compareF|])
, (U.ConType [t|ArchAddrWidthRepr|] `U.TypeApp` U.AnyType, [|compareF|])
]) ])
instance FunctorFC (MacawExprExtension arch) where instance FunctorFC (MacawExprExtension arch) where

134
symbolic/src/Data/Macaw/Symbolic/MemOps.hs
View File

@ -67,7 +67,7 @@ import Lang.Crucible.LLVM.MemModel.Generic(ppPtr)
import Lang.Crucible.LLVM.DataLayout(EndianForm(..)) import Lang.Crucible.LLVM.DataLayout(EndianForm(..))
import Lang.Crucible.LLVM.Bytes(toBytes) import Lang.Crucible.LLVM.Bytes(toBytes)
import Data.Macaw.Symbolic.CrucGen(lemma1_16) import Data.Macaw.Symbolic.CrucGen (addrWidthIsPos)
import Data.Macaw.Symbolic.PersistentState(ToCrucibleType) import Data.Macaw.Symbolic.PersistentState(ToCrucibleType)
import Data.Macaw.CFG.Core(MemRepr(BVMemRepr)) import Data.Macaw.CFG.Core(MemRepr(BVMemRepr))
import qualified Data.Macaw.Memory as M import qualified Data.Macaw.Memory as M
@ -105,8 +105,12 @@ doMakeCall k st mvar regs =
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
addrWidthAtLeast16 :: M.AddrWidthRepr w -> LeqProof 16 w
addrWidthAtLeast16 M.Addr32 = LeqProof
addrWidthAtLeast16 M.Addr64 = LeqProof
doGetGlobal :: doGetGlobal ::
(IsSymInterface sym, 16 <= w, M.MemWidth w) => (IsSymInterface sym, M.MemWidth w) =>
CrucibleState s sym ext rtp blocks r ctx {- ^ Simulator state -} -> CrucibleState s sym ext rtp blocks r ctx {- ^ Simulator state -} ->
GlobalVar Mem {- ^ Model of memory -} -> GlobalVar Mem {- ^ Model of memory -} ->
Map M.RegionIndex (RegValue sym (LLVMPointerType w)) {- ^ Region ptrs -} -> Map M.RegionIndex (RegValue sym (LLVMPointerType w)) {- ^ Region ptrs -} ->
@ -124,10 +128,11 @@ doGetGlobal st mvar globs addr =
Just region -> Just region ->
do mem <- getMem st mvar do mem <- getMem st mvar
let sym = stateSymInterface st let sym = stateSymInterface st
let w = M.addrWidthNatRepr (M.addrWidthRepr addr) let w = M.addrWidthRepr addr
off <- bvLit sym w (M.memWordInteger (M.addrOffset addr)) LeqProof <- pure $ addrWidthAtLeast16 w
res <- let ?ptrWidth = w let ?ptrWidth = M.addrWidthNatRepr w
in doPtrAddOffset sym mem region off off <- bvLit sym ?ptrWidth (M.memWordInteger (M.addrOffset addr))
res <- doPtrAddOffset sym mem region off
return (res, st) return (res, st)
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
@ -137,10 +142,10 @@ doGetGlobal st mvar globs addr =
-- state, we don't actually do it. -- state, we don't actually do it.
type PtrOp sym w a = type PtrOp sym w a =
forall s ext rtp blocks r ctx. forall s ext rtp blocks r ctx.
(IsSymInterface sym, 16 <= w) => IsSymInterface sym =>
CrucibleState s sym ext rtp blocks r ctx {- ^ Simulator state -} -> CrucibleState s sym ext rtp blocks r ctx {- ^ Simulator state -} ->
GlobalVar Mem {- ^ Memory model -} -> GlobalVar Mem {- ^ Memory model -} ->
NatRepr w {- ^ Width of pointer -} -> M.AddrWidthRepr w {- ^ Width of pointer -} ->
RegEntry sym (LLVMPointerType w) {- ^ Argument 1 -} -> RegEntry sym (LLVMPointerType w) {- ^ Argument 1 -} ->
RegEntry sym (LLVMPointerType w) {- ^ Argument 2 -} -> RegEntry sym (LLVMPointerType w) {- ^ Argument 2 -} ->
IO (a, CrucibleState s sym ext rtp blocks r ctx) IO (a, CrucibleState s sym ext rtp blocks r ctx)
@ -154,11 +159,18 @@ binOpLabel lab x y =
, "}" , "}"
] ]
mkUndefinedPtr :: (IsSymInterface sym, 1 <= w) =>
sym -> String -> NatRepr w -> IO (LLVMPtr sym w)
mkUndefinedPtr sym nm w =
do base <- mkUndefined sym ("ptr_base_" ++ nm) BaseNatRepr
off <- mkUndefinedBV sym ("ptr_offset_" ++ nm) w
return (LLVMPointer base off)
doPtrMux :: Pred sym -> PtrOp sym w (LLVMPtr sym w) doPtrMux :: Pred sym -> PtrOp sym w (LLVMPtr sym w)
doPtrMux c = ptrOp $ \sym _ w xPtr xBits yPtr yBits x y -> doPtrMux c = ptrOp $ \sym _ w xPtr xBits yPtr yBits x y ->
do both_bits <- andPred sym xBits yBits do both_bits <- andPred sym xBits yBits
both_ptrs <- andPred sym xPtr yPtr both_ptrs <- andPred sym xPtr yPtr
undef <- mkUndefinedPtr sym "ptr_mux" w undef <- mkUndefinedPtr sym "ptr_mux" (M.addrWidthNatRepr w)
cases sym (binOpLabel "ptr_mux" x y) muxLLVMPtr (Just undef) cases sym (binOpLabel "ptr_mux" x y) muxLLVMPtr (Just undef)
[ both_bits ~> [ both_bits ~>
endCase =<< llvmPointer_bv sym =<< bvIte sym c (asBits x) (asBits y) endCase =<< llvmPointer_bv sym =<< bvIte sym c (asBits x) (asBits y)
@ -171,26 +183,27 @@ doPtrAdd = ptrOp $ \sym _ w xPtr xBits yPtr yBits x y ->
do both_bits <- andPred sym xBits yBits do both_bits <- andPred sym xBits yBits
ptr_bits <- andPred sym xPtr yBits ptr_bits <- andPred sym xPtr yBits
bits_ptr <- andPred sym xBits yPtr bits_ptr <- andPred sym xBits yPtr
let nw = M.addrWidthNatRepr w
a <- cases sym (binOpLabel "ptr_add" x y) muxLLVMPtr Nothing a <- cases sym (binOpLabel "ptr_add" x y) muxLLVMPtr Nothing
[ both_bits ~> [ both_bits ~>
endCase =<< llvmPointer_bv sym =<< bvAdd sym (asBits x) (asBits y) endCase =<< llvmPointer_bv sym =<< bvAdd sym (asBits x) (asBits y)
, ptr_bits ~> endCase =<< ptrAdd sym w x (asBits y) , ptr_bits ~> endCase =<< ptrAdd sym nw x (asBits y)
, bits_ptr ~> endCase =<< ptrAdd sym w y (asBits x) , bits_ptr ~> endCase =<< ptrAdd sym nw y (asBits x)
] ]
return a return a
isValidPtr :: isValidPtr ::
(IsSymInterface sym, 16 <= w) => (IsSymInterface sym) =>
sym -> sym ->
RegValue sym Mem -> RegValue sym Mem ->
NatRepr w -> M.AddrWidthRepr w ->
LLVMPtr sym w -> LLVMPtr sym w ->
IO (Pred sym) IO (Pred sym)
isValidPtr sym mem w p = isValidPtr sym mem w p =
do let ?ptrWidth = w do LeqProof <- pure $ addrWidthIsPos w
LeqProof <- return (lemma1_16 w) LeqProof <- pure $ addrWidthAtLeast16 w
let ?ptrWidth = M.addrWidthNatRepr w
isValidPointer sym p mem isValidPointer sym p mem
doPtrSub :: PtrOp sym w (LLVMPtr sym w) doPtrSub :: PtrOp sym w (LLVMPtr sym w)
@ -198,12 +211,13 @@ doPtrSub = ptrOp $ \sym mem w xPtr xBits yPtr yBits x y ->
do both_bits <- andPred sym xBits yBits do both_bits <- andPred sym xBits yBits
ptr_bits <- andPred sym xPtr yBits ptr_bits <- andPred sym xPtr yBits
ptr_ptr <- andPred sym xPtr yPtr ptr_ptr <- andPred sym xPtr yPtr
let nw = M.addrWidthNatRepr w
cases sym (binOpLabel "ptr_sub" x y) muxLLVMPtr Nothing cases sym (binOpLabel "ptr_sub" x y) muxLLVMPtr Nothing
[ both_bits ~> [ both_bits ~>
endCase =<< llvmPointer_bv sym =<< bvSub sym (asBits x) (asBits y) endCase =<< llvmPointer_bv sym =<< bvSub sym (asBits x) (asBits y)
, ptr_bits ~> endCase =<< ptrSub sym w x (asBits y) , ptr_bits ~> endCase =<< ptrSub sym nw x (asBits y)
, ptr_ptr ~> , ptr_ptr ~>
do okP1 <- isValidPtr sym mem w x do okP1 <- isValidPtr sym mem w x
@ -215,10 +229,11 @@ doPtrSub = ptrOp $ \sym mem w xPtr xBits yPtr yBits x y ->
] ]
doPtrAnd :: PtrOp sym w (LLVMPtr sym w) doPtrAnd :: PtrOp sym w (LLVMPtr sym w)
doPtrAnd = ptrOp $ \sym mem w xPtr xBits yPtr yBits x y -> doPtrAnd = ptrOp $ \sym _mem w xPtr xBits yPtr yBits x y ->
let doPtrAlign amt isP isB v let nw = M.addrWidthNatRepr w
doPtrAlign amt isP isB v
| amt == 0 = return v | amt == 0 = return v
| amt == natValue w = mkNullPointer sym w | amt == natValue nw = mkNullPointer sym nw
| Just 0 <- asNat (ptrBase v) = llvmPointer_bv sym =<< | Just 0 <- asNat (ptrBase v) = llvmPointer_bv sym =<<
bvAndBits sym (asBits x) (asBits y) bvAndBits sym (asBits x) (asBits y)
@ -234,26 +249,25 @@ doPtrAnd = ptrOp $ \sym mem w xPtr xBits yPtr yBits x y ->
nm <- mkName "align_amount" nm <- mkName "align_amount"
least <- freshConstant sym nm (BaseBVRepr n) least <- freshConstant sym nm (BaseBVRepr n)
Just LeqProof <- return (testLeq n w) Just LeqProof <- return (testLeq n nw)
let mostBits = subNat w n let mostBits = subNat nw n
Just LeqProof <- return (testLeq (knownNat @1) mostBits) Just LeqProof <- return (testLeq (knownNat @1) mostBits)
most <- bvLit sym mostBits 0 most <- bvLit sym mostBits 0
bts <- bvConcat sym most least bts <- bvConcat sym most least
Refl <- return (minusPlusCancel w n) Refl <- return (minusPlusCancel nw n)
endCase =<< ptrSub sym w v bts endCase =<< ptrSub sym nw v bts
-- We don't check for the validity of the pointer: -- We don't check for the validity of the pointer:
-- this is done upon use. -- this is done upon use.
] ]
in in case (isAlignMask x, isAlignMask y) of
case (isAlignMask x, isAlignMask y) of (Just yes, _) -> doPtrAlign yes yPtr yBits y
(Just yes, _) -> doPtrAlign yes yPtr yBits y (_, Just yes) -> doPtrAlign yes xPtr xBits x
(_, Just yes) -> doPtrAlign yes xPtr xBits x _ -> do v1 <- doPtrToBits sym nw x
_ -> do v1 <- doPtrToBits sym w x v2 <- doPtrToBits sym nw y
v2 <- doPtrToBits sym w y llvmPointer_bv sym =<< bvAndBits sym v1 v2
llvmPointer_bv sym =<< bvAndBits sym v1 v2
@ -290,21 +304,22 @@ doPtrEq = ptrOp $ \sym mem w xPtr xBits yPtr yBits x y ->
do both_bits <- andPred sym xBits yBits do both_bits <- andPred sym xBits yBits
both_ptrs <- andPred sym xPtr yPtr both_ptrs <- andPred sym xPtr yPtr
undef <- mkUndefinedBool sym "ptr_eq" undef <- mkUndefinedBool sym "ptr_eq"
let nw = M.addrWidthNatRepr w
cases sym (binOpLabel "ptr_eq" x y) itePred (Just undef) cases sym (binOpLabel "ptr_eq" x y) itePred (Just undef)
[ both_bits ~> endCase =<< bvEq sym (asBits x) (asBits y) [ both_bits ~> endCase =<< bvEq sym (asBits x) (asBits y)
, both_ptrs ~> , both_ptrs ~>
do okP1 <- isValidPtr sym mem w x do okP1 <- isValidPtr sym mem w x
okP2 <- isValidPtr sym mem w y okP2 <- isValidPtr sym mem w y
ok <- andPred sym okP1 okP2 ok <- andPred sym okP1 okP2
endCaseCheck ok "Comparing invalid pointers" =<< ptrEq sym w x y endCaseCheck ok "Comparing invalid pointers" =<< ptrEq sym nw x y
] ]
doReadMem :: doReadMem ::
(IsSymInterface sym, 16 <= ptrW) => IsSymInterface sym =>
CrucibleState s sym ext rtp blocks r ctx {- ^ Simulator state -} -> CrucibleState s sym ext rtp blocks r ctx {- ^ Simulator state -} ->
GlobalVar Mem -> GlobalVar Mem ->
Map M.RegionIndex (RegValue sym (LLVMPointerType ptrW)) {- ^ Region ptrs -} -> Map M.RegionIndex (RegValue sym (LLVMPointerType ptrW)) {- ^ Region ptrs -} ->
NatRepr ptrW -> M.AddrWidthRepr ptrW ->
MemRepr ty -> MemRepr ty ->
RegEntry sym (LLVMPointerType ptrW) -> RegEntry sym (LLVMPointerType ptrW) ->
IO ( RegValue sym (ToCrucibleType ty) IO ( RegValue sym (ToCrucibleType ty)
@ -318,16 +333,18 @@ doReadMem st mvar globs w (BVMemRepr bytes endian) ptr0 =
ty = bitvectorType (toBytes (widthVal bytes)) ty = bitvectorType (toBytes (widthVal bytes))
bitw = natMultiply (knownNat @8) bytes bitw = natMultiply (knownNat @8) bytes
LeqProof <- return (lemma1_16 w)
LeqProof <- return (leqMulPos (knownNat @8) bytes) LeqProof <- return (leqMulPos (knownNat @8) bytes)
ptr <- tryGlobPtr sym mem globs w (regValue ptr0) ptr <- tryGlobPtr sym mem globs w (regValue ptr0)
let ?ptrWidth = M.addrWidthNatRepr w
ok <- isValidPtr sym mem w ptr ok <- isValidPtr sym mem w ptr
check sym ok "doReadMem" check sym ok "doReadMem"
$ "Reading through an invalid pointer: " ++ show (ppPtr ptr) $ "Reading through an invalid pointer: " ++ show (ppPtr ptr)
val <- let ?ptrWidth = w in loadRaw sym mem ptr ty LeqProof <- pure $ addrWidthIsPos w
LeqProof <- pure $ addrWidthAtLeast16 w
val <- loadRaw sym mem ptr ty
a <- case valToBits bitw val of a <- case valToBits bitw val of
Just a -> return a Just a -> return a
Nothing -> fail "[doReadMem] We read an unexpected value" Nothing -> fail "[doReadMem] We read an unexpected value"
@ -337,11 +354,11 @@ doReadMem st mvar globs w (BVMemRepr bytes endian) ptr0 =
doCondReadMem :: doCondReadMem ::
(IsSymInterface sym, 16 <= ptrW) => IsSymInterface sym =>
CrucibleState s sym ext rtp blocks r ctx {- ^ Simulator state -} -> CrucibleState s sym ext rtp blocks r ctx {- ^ Simulator state -} ->
GlobalVar Mem {- ^ Memory model -} -> GlobalVar Mem {- ^ Memory model -} ->
Map M.RegionIndex (RegValue sym (LLVMPointerType ptrW)) {- ^ Region ptrs -} -> Map M.RegionIndex (RegValue sym (LLVMPointerType ptrW)) {- ^ Region ptrs -} ->
NatRepr ptrW {- ^ Width of ptr -} -> M.AddrWidthRepr ptrW {- ^ Width of ptr -} ->
MemRepr ty {- ^ What/how we are reading -} -> MemRepr ty {- ^ What/how we are reading -} ->
RegEntry sym BoolType {- ^ Condition -} -> RegEntry sym BoolType {- ^ Condition -} ->
RegEntry sym (LLVMPointerType ptrW) {- ^ Pointer -} -> RegEntry sym (LLVMPointerType ptrW) {- ^ Pointer -} ->
@ -358,7 +375,6 @@ doCondReadMem st mvar globs w (BVMemRepr bytes endian) cond0 ptr0 def0 =
ty = bitvectorType (toBytes (widthVal bytes)) ty = bitvectorType (toBytes (widthVal bytes))
bitw = natMultiply (knownNat @8) bytes bitw = natMultiply (knownNat @8) bytes
LeqProof <- return (lemma1_16 w)
LeqProof <- return (leqMulPos (knownNat @8) bytes) LeqProof <- return (leqMulPos (knownNat @8) bytes)
ptr <- tryGlobPtr sym mem globs w (regValue ptr0) ptr <- tryGlobPtr sym mem globs w (regValue ptr0)
@ -367,7 +383,9 @@ doCondReadMem st mvar globs w (BVMemRepr bytes endian) cond0 ptr0 def0 =
$ "Conditional read through an invalid pointer: " ++ $ "Conditional read through an invalid pointer: " ++
show (ppPtr ptr) show (ppPtr ptr)
val <- let ?ptrWidth = w in loadRawWithCondition sym mem ptr ty LeqProof <- pure $ addrWidthIsPos w
LeqProof <- pure $ addrWidthAtLeast16 w
val <- let ?ptrWidth = M.addrWidthNatRepr w in loadRawWithCondition sym mem ptr ty
let useDefault msg = let useDefault msg =
do notC <- notPred sym cond do notC <- notPred sym cond
@ -387,11 +405,11 @@ doCondReadMem st mvar globs w (BVMemRepr bytes endian) cond0 ptr0 def0 =
doWriteMem :: doWriteMem ::
(IsSymInterface sym, 16 <= ptrW) => IsSymInterface sym =>
CrucibleState s sym ext rtp blocks r ctx {- ^ Simulator state -} -> CrucibleState s sym ext rtp blocks r ctx {- ^ Simulator state -} ->
GlobalVar Mem {- ^ Memory model -} -> GlobalVar Mem {- ^ Memory model -} ->
Map M.RegionIndex (RegValue sym (LLVMPointerType ptrW)) {- ^ Region ptrs -} -> Map M.RegionIndex (RegValue sym (LLVMPointerType ptrW)) {- ^ Region ptrs -} ->
NatRepr ptrW {- ^ Width of ptr -} -> M.AddrWidthRepr ptrW {- ^ Width of ptr -} ->
MemRepr ty {- ^ What/how we are writing -} -> MemRepr ty {- ^ What/how we are writing -} ->
RegEntry sym (LLVMPointerType ptrW) {- ^ Pointer -} -> RegEntry sym (LLVMPointerType ptrW) {- ^ Pointer -} ->
RegEntry sym (ToCrucibleType ty) {- ^ Write this value -} -> RegEntry sym (ToCrucibleType ty) {- ^ Write this value -} ->
@ -405,7 +423,8 @@ doWriteMem st mvar globs w (BVMemRepr bytes endian) ptr0 val =
let sym = stateSymInterface st let sym = stateSymInterface st
ty = bitvectorType (toBytes (widthVal bytes)) ty = bitvectorType (toBytes (widthVal bytes))
LeqProof <- return (lemma1_16 w) LeqProof <- pure $ addrWidthIsPos w
LeqProof <- pure $ addrWidthAtLeast16 w
LeqProof <- return (leqMulPos (knownNat @8) bytes) LeqProof <- return (leqMulPos (knownNat @8) bytes)
ptr <- tryGlobPtr sym mem globs w (regValue ptr0) ptr <- tryGlobPtr sym mem globs w (regValue ptr0)
@ -413,16 +432,12 @@ doWriteMem st mvar globs w (BVMemRepr bytes endian) ptr0 val =
check sym ok "doWriteMem" check sym ok "doWriteMem"
$ "Write to an invalid location: " ++ show (ppPtr ptr) $ "Write to an invalid location: " ++ show (ppPtr ptr)
let ?ptrWidth = w let ?ptrWidth = M.addrWidthNatRepr w
let v0 = regValue val let v0 = regValue val
v = LLVMValInt (ptrBase v0) (asBits v0) v = LLVMValInt (ptrBase v0) (asBits v0)
mem1 <- storeRaw sym mem ptr ty v mem1 <- storeRaw sym mem ptr ty v
return ((), setMem st mvar mem1) return ((), setMem st mvar mem1)
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
-- Utilities -- Utilities
@ -455,14 +470,14 @@ ptrOp ::
( (1 <= w) => ( (1 <= w) =>
sym -> sym ->
RegValue sym Mem -> RegValue sym Mem ->
NatRepr w -> M.AddrWidthRepr w ->
Pred sym -> Pred sym -> Pred sym -> Pred sym -> Pred sym -> Pred sym -> Pred sym -> Pred sym ->
LLVMPtr sym w -> LLVMPtr sym w -> IO a LLVMPtr sym w -> LLVMPtr sym w -> IO a
) -> ) ->
PtrOp sym w a PtrOp sym w a
ptrOp k st mvar w x0 y0 = ptrOp k st mvar w x0 y0 =
do mem <- getMem st mvar do mem <- getMem st mvar
LeqProof <- return (lemma1_16 w) LeqProof <- return (addrWidthIsPos w)
let sym = stateSymInterface st let sym = stateSymInterface st
x = regValue x0 x = regValue x0
y = regValue y0 y = regValue y0
@ -560,13 +575,6 @@ checkEndian mem endian =
, " *** Read : " ++ show need ] , " *** Read : " ++ show need ]
mkUndefinedPtr :: (IsSymInterface sym, 1 <= w) =>
sym -> String -> NatRepr w -> IO (LLVMPtr sym w)
mkUndefinedPtr sym nm w =
do base <- mkUndefined sym ("ptr_base_" ++ nm) BaseNatRepr
off <- mkUndefinedBV sym ("ptr_offset_" ++ nm) w
return (LLVMPointer base off)
-- | A fresh boolean variable -- | A fresh boolean variable
mkUndefinedBool :: mkUndefinedBool ::
(IsSymInterface sym) => sym -> String -> IO (RegValue sym BoolType) (IsSymInterface sym) => sym -> String -> IO (RegValue sym BoolType)
@ -608,18 +616,19 @@ which is statically known to be a constant, we consult
the global map to see if we know about a correpsonding the global map to see if we know about a correpsonding
addres.. If so, we use that for the memory operation. -} addres.. If so, we use that for the memory operation. -}
tryGlobPtr :: tryGlobPtr ::
(IsSymInterface sym, 16 <= w) => IsSymInterface sym =>
sym -> sym ->
RegValue sym Mem -> RegValue sym Mem ->
Map M.RegionIndex (RegValue sym (LLVMPointerType w)) {- ^ Region ptrs -} -> Map M.RegionIndex (RegValue sym (LLVMPointerType w)) {- ^ Region ptrs -} ->
NatRepr w -> M.AddrWidthRepr w ->
LLVMPtr sym w -> LLVMPtr sym w ->
IO (LLVMPtr sym w) IO (LLVMPtr sym w)
tryGlobPtr sym mem globs w val tryGlobPtr sym mem globs w val
| Just 0 <- asNat (ptrBase val) | Just 0 <- asNat (ptrBase val)
, Just r <- Map.lookup literalAddrRegion globs , Just r <- Map.lookup literalAddrRegion globs
, LeqProof <- lemma1_16 w , LeqProof <- addrWidthIsPos w
= let ?ptrWidth = w , LeqProof <- addrWidthAtLeast16 w =
let ?ptrWidth = M.addrWidthNatRepr w
in doPtrAddOffset sym mem r (asBits val) in doPtrAddOffset sym mem r (asBits val)
| otherwise = return val | otherwise = return val
where where
@ -635,6 +644,3 @@ isAlignMask v =
let (zeros,ones) = break (testBit k) (take w [ 0 .. ]) let (zeros,ones) = break (testBit k) (take w [ 0 .. ])
guard (all (testBit k) ones) guard (all (testBit k) ones)
return (fromIntegral (length zeros)) return (fromIntegral (length zeros))

3
x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
View File

@ -101,8 +101,6 @@ getReg ::
forall n t f. (Idx n (ArchRegContext M.X86_64) t) => RegAssign f -> f t forall n t f. (Idx n (ArchRegContext M.X86_64) t) => RegAssign f -> f t
getReg x = x ^. (field @n) getReg x = x ^. (field @n)
x86RegName :: M.X86Reg tp -> C.SolverSymbol x86RegName :: M.X86Reg tp -> C.SolverSymbol
x86RegName M.X86_IP = C.systemSymbol "!ip" x86RegName M.X86_IP = C.systemSymbol "!ip"
x86RegName (M.X86_GP r) = C.systemSymbol $ "!" ++ show r x86RegName (M.X86_GP r) = C.systemSymbol $ "!" ++ show r
@ -250,4 +248,3 @@ x86_64MacawSymbolicFns =
x86_64MacawEvalFn :: x86_64MacawEvalFn ::
C.IsSymInterface sym => SymFuns sym -> MacawArchEvalFn sym M.X86_64 C.IsSymInterface sym => SymFuns sym -> MacawArchEvalFn sym M.X86_64
x86_64MacawEvalFn fs (X86PrimFn x) s = semantics fs x s x86_64MacawEvalFn fs (X86PrimFn x) s = semantics fs x s