GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-11-24 08:53:12 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #27 from GaloisInc/jhx/vec

Browse Source 
Add vector type and operations.
This commit is contained in:
Joe Hendrix 2019-02-27 08:57:50 -08:00 committed by GitHub
commit e204724358
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
23 changed files with 1252 additions and 1018 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
.gitignore vendored
View File

@ -6,6 +6,7 @@ dist-newstyle/
cabal.sandbox.config
.cabal-sandbox
.stack-work/
stack.yaml
TAGS
.ghc.environment.*
**/tests/samples/*.last-actual

43
.travis.yml
View File

@ -1,42 +1,29 @@
# This file has been generated -- see https://github.com/hvr/multi-ghc-travis
language: c
sudo: false
language: minimal
git:
submodules: false # whether to recursively clone submodules
cache:
directories:
- $HOME/.cabsnap
- $HOME/.cabal/packages
before_cache:
- rm -fv $HOME/.cabal/packages/hackage.haskell.org/build-reports.log
- rm -fv $HOME/.cabal/packages/hackage.haskell.org/00-index.tar
matrix:
include:
- env: CABALVER=1.24 GHCVER=8.2.2
compiler: ": #GHC 8.2.2"
addons: {apt: {packages: [cabal-install-1.24,ghc-8.2.2], sources: [hvr-ghc]}}
- $HOME/.stack
before_install:
- unset CC
- mkdir -p ~/.local/bin
- export PATH=$HOME/.local/bin:/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH
- travis_retry curl -L https://www.stackage.org/stack/linux-x86_64 | tar xz --wildcards --strip-components=1 -C ~/.local/bin '*/stack'
# This is an unfortunate hack that changes ssh paths into http path, so that
# we can do a read-only clone of our submodules without worrying about ssh
# keys.
- sed -i 's/git@github.com:/https:\/\/github.com\//' .gitmodules
- git submodule update --init
# Download and unpack the stack executable
- mkdir -p $HOME/.local/bin
- export PATH=$HOME/.local/bin:$PATH
- travis_retry curl -L https://get.haskellstack.org/stable/linux-x86_64.tar.gz | tar xz --wildcards --strip-components=1 -C ~/.local/bin '*/stack'
install:
- cabal --version
- echo "$(ghc --version) [$(ghc --print-project-git-commit-id 2> /dev/null || echo '?')]"
- if [ -f $HOME/.cabal/packages/hackage.haskell.org/00-index.tar.gz ];
then
zcat $HOME/.cabal/packages/hackage.haskell.org/00-index.tar.gz >
$HOME/.cabal/packages/hackage.haskell.org/00-index.tar;
fi
- travis_retry cabal update -v
- sed -i 's/^jobs:/-- jobs:/' ${HOME}/.cabal/config
- travis_wait stack --no-terminal --skip-ghc-check setup
# Here starts the actual work to be performed for the package under test;
# any command which exits with a non-zero exit code causes the build to fail.
script:
- travis_wait stack --no-terminal --skip-ghc-check setup
- stack --stack-yaml stack.ghc-8.6.3.yaml build macaw-x86 macaw-x86-symbolic
- stack --stack-yaml stack.ghc-8.6.3.yaml test macaw-x86

2
base/src/Data/Macaw/CFG.hs
View File

@ -8,8 +8,10 @@ module Data.Macaw.CFG
( module Data.Macaw.CFG.Core
, module Data.Macaw.CFG.App
, module Data.Macaw.Memory
, Data.Macaw.Types.FloatInfoRepr(..)
) where
import Data.Macaw.CFG.App
import Data.Macaw.CFG.Core
import qualified Data.Macaw.Types
import Data.Macaw.Memory

93
base/src/Data/Macaw/CFG/App.hs
View File

@ -19,6 +19,11 @@ module Data.Macaw.CFG.App
( App(..)
, ppApp
, ppAppA
-- * Casting proof objects.
, WidthEqProof(..)
, widthEqTarget
, widthEqProofEq
, widthEqProofCompare
) where
import qualified Data.Kind as Kind
@ -36,6 +41,78 @@ import Data.Macaw.Utils.Pretty
-----------------------------------------------------------------------
-- App
-- | Data type to represent that two types use the same number of
-- bits, and thus can be bitcast.
--
-- Note. This datatype needs to balance several competing
-- requirements. It needs to support all bitcasts needed by
-- architectures, represent bitcasts compactly, allow bitcasts to be
-- removed during optimization, and allow bitcasts to be symbolically
-- simulated.
--
-- Due to these requirements, we have a fairly limited set of proof
-- rules. New rules can be added, but need to be balanced against the
-- above set of goals. By design we do not have transitivity or
-- equality, as those can be obtained by respectively chaining
-- bitcasts or eliminating them.
data WidthEqProof (in_tp :: Type) (out_tp :: Type) where
PackBits :: (1 <= n, 2 <= n, 1 <= w)
=> !(NatRepr n)
-> !(NatRepr w)
-> WidthEqProof (VecType n (BVType w)) (BVType (n * w))
UnpackBits :: (1 <= n, 2 <= n, 1 <= w)
=> !(NatRepr n)
-> !(NatRepr w)
-> WidthEqProof (BVType (n * w)) (VecType n (BVType w))
FromFloat :: !(FloatInfoRepr ftp)
-> WidthEqProof (FloatType ftp) (BVType (FloatInfoBits ftp))
ToFloat :: !(FloatInfoRepr ftp)
-> WidthEqProof (BVType (FloatInfoBits ftp)) (FloatType ftp)
VecEqCongruence :: !(NatRepr n)
-> !(WidthEqProof i o)
-> WidthEqProof (VecType n i) (VecType n o)
-- | Return the result type of the width equality proof
widthEqTarget :: WidthEqProof i o -> TypeRepr o
widthEqTarget (PackBits n w) =
case leqMulPos n w of
LeqProof -> BVTypeRepr (natMultiply n w)
widthEqTarget (UnpackBits n w) = VecTypeRepr n (BVTypeRepr w)
widthEqTarget (FromFloat f) =
case floatInfoBitsIsPos f of
LeqProof -> BVTypeRepr (floatInfoBits f)
widthEqTarget (ToFloat f) = FloatTypeRepr f
widthEqTarget (VecEqCongruence n r) = VecTypeRepr n (widthEqTarget r)
-- Force app to be in template-haskell context.
$(pure [])
widthEqProofEq :: WidthEqProof xi xo
-> WidthEqProof yi yo
-> Maybe (WidthEqProof xi xo :~: WidthEqProof yi yo)
widthEqProofEq =
$(structuralTypeEquality [t|WidthEqProof|]
[ (ConType [t|NatRepr|] `TypeApp` AnyType, [|testEquality|])
, (ConType [t|FloatInfoRepr|] `TypeApp` AnyType, [|testEquality|])
, (ConType [t|WidthEqProof|] `TypeApp` AnyType `TypeApp` AnyType,
[|widthEqProofEq|])
]
)
widthEqProofCompare :: WidthEqProof xi xo
-> WidthEqProof yi yo
-> OrderingF (WidthEqProof xi xo) (WidthEqProof yi yo)
widthEqProofCompare =
$(structuralTypeOrd [t|WidthEqProof|]
[ (ConType [t|NatRepr|] `TypeApp` AnyType, [|compareF|])
, (ConType [t|FloatInfoRepr|] `TypeApp` AnyType, [|compareF|])
, (ConType [t|WidthEqProof|] `TypeApp` AnyType `TypeApp` AnyType,
[|widthEqProofCompare|])
]
)
-- | This datatype defines operations used on multiple architectures.
--
-- These operations are all total functions. Different architecture tend to have
@ -43,7 +120,7 @@ import Data.Macaw.Utils.Pretty
-- all architecture specific.
data App (f :: Type -> Kind.Type) (tp :: Type) where
-- Compare for equality.
-- | Compare for equality.
Eq :: !(f tp) -> !(f tp) -> App f BoolType
Mux :: !(TypeRepr tp) -> !(f BoolType) -> !(f tp) -> !(f tp) -> App f tp
@ -68,15 +145,15 @@ data App (f :: Type -> Kind.Type) (tp :: Type) where
-- | Given a @m@-bit bitvector @x@ and a natural number @n@ greater than @m@, this returns
-- the bitvector with the same @m@ least signficant bits, and where the new bits are
-- the same as the most significant bit in @x@.
SExt :: (1 <= m, m+1 <= n, 1 <= n) => f (BVType m) -> NatRepr n -> App f (BVType n)
SExt :: (1 <= m, m+1 <= n, 1 <= n) => !(f (BVType m)) -> !(NatRepr n) -> App f (BVType n)
-- | Given a @m@-bit bitvector @x@ and a natural number @n@ greater than @m@, this returns
-- the bitvector with the same @m@ least signficant bits, and where the new bits are
-- all @false@.
UExt :: (1 <= m, m+1 <= n, 1 <= n) => f (BVType m) -> NatRepr n -> App f (BVType n)
UExt :: (1 <= m, m+1 <= n, 1 <= n) => !(f (BVType m)) -> !(NatRepr n) -> App f (BVType n)
-- | This casts an expression from one type to another that should
-- use the same number of bytes in memory.
Bitcast :: f tp -> TypeRepr out -> App f out
Bitcast :: !(f tp) -> !(WidthEqProof tp out) -> App f out
----------------------------------------------------------------------
-- Bitvector operations
@ -214,6 +291,8 @@ instance TestEquality f => TestEquality (App f) where
[|testEquality|])
, (ConType [t|P.Index|] `TypeApp` AnyType `TypeApp` AnyType,
[|testEquality|])
, (ConType [t|WidthEqProof|] `TypeApp` AnyType `TypeApp` AnyType,
[|widthEqProofEq|])
]
)
@ -227,6 +306,8 @@ instance OrdF f => OrdF (App f) where
[|compareF|])
, (ConType [t|P.Index|] `TypeApp` AnyType `TypeApp` AnyType,
[|compareF|])
, (ConType [t|WidthEqProof|] `TypeApp` AnyType `TypeApp` AnyType,
[|widthEqProofCompare|])
]
)
@ -271,7 +352,7 @@ ppAppA pp a0 =
Trunc x w -> sexprA "trunc" [ pp x, ppNat w ]
SExt x w -> sexprA "sext" [ pp x, ppNat w ]
UExt x w -> sexprA "uext" [ pp x, ppNat w ]
Bitcast x tp -> sexprA "bitcast" [ pp x, pure (text (show tp)) ]
Bitcast x tp -> sexprA "bitcast" [ pp x, pure (text (show (widthEqTarget tp))) ]
BVAdd _ x y -> sexprA "bv_add" [ pp x, pp y ]
BVAdc _ x y c -> sexprA "bv_adc" [ pp x, pp y, pp c ]
BVSub _ x y -> sexprA "bv_sub" [ pp x, pp y ]
@ -316,7 +397,7 @@ instance HasRepr (App f) TypeRepr where
Trunc _ w -> BVTypeRepr w
SExt _ w -> BVTypeRepr w
UExt _ w -> BVTypeRepr w
Bitcast _ tp -> tp
Bitcast _ p -> widthEqTarget p
AndApp{} -> knownRepr
OrApp{} -> knownRepr

48
base/src/Data/Macaw/CFG/AssignRhs.hs
View File

@ -104,10 +104,22 @@ type ArchMemAddr arch = MemAddr (ArchAddrWidth arch)
data MemRepr (tp :: Type) where
-- | Denotes a bitvector with the given number of bytes and endianness.
BVMemRepr :: (1 <= w) => !(NatRepr w) -> !Endianness -> MemRepr (BVType (8*w))
-- | A floating point value (stored in given endianness.
FloatMemRepr :: !(FloatInfoRepr f) -> !Endianness -> MemRepr (FloatType f)
-- | A vector of values with zero entry first.
--
-- The first value is stored at the address, the second is stored at address + sizeof eltType,
-- etc.
PackedVecMemRepr :: !(NatRepr n) -> !(MemRepr tp) -> MemRepr (VecType n tp)
ppEndianness :: Endianness -> String
ppEndianness LittleEndian = "le"
ppEndianness BigEndian = "be"
instance Pretty (MemRepr tp) where
pretty (BVMemRepr w BigEndian) = text "bvbe" <+> text (show w)
pretty (BVMemRepr w LittleEndian) = text "bvle" <+> text (show w)
pretty (BVMemRepr w end) = text "bv" <> text (ppEndianness end) <> text (show w)
pretty (FloatMemRepr f end) = pretty f <> text (ppEndianness end)
pretty (PackedVecMemRepr w r) = text "v" <> text (show w) <> pretty r
instance Show (MemRepr tp) where
show = show . pretty
@ -115,25 +127,45 @@ instance Show (MemRepr tp) where
-- | Return the number of bytes this uses in memory.
memReprBytes :: MemRepr tp -> Integer
memReprBytes (BVMemRepr x _) = intValue x
memReprBytes (FloatMemRepr f _) = intValue (floatInfoBytes f)
memReprBytes (PackedVecMemRepr w r) = intValue w * memReprBytes r
instance TestEquality MemRepr where
testEquality (BVMemRepr xw xe) (BVMemRepr yw ye) =
if xe == ye then do
Refl <- testEquality xw yw
Just Refl
else
Nothing
testEquality (BVMemRepr xw xe) (BVMemRepr yw ye) = do
Refl <- testEquality xw yw
if xe == ye then Just Refl else Nothing
testEquality (FloatMemRepr xf xe) (FloatMemRepr yf ye) = do
Refl <- testEquality xf yf
if xe == ye then Just Refl else Nothing
testEquality (PackedVecMemRepr xn xe) (PackedVecMemRepr yn ye) = do
Refl <- testEquality xn yn
Refl <- testEquality xe ye
Just Refl
testEquality _ _ = Nothing
instance OrdF MemRepr where
compareF (BVMemRepr xw xe) (BVMemRepr yw ye) =
joinOrderingF (compareF xw yw) $
fromOrdering (compare xe ye)
compareF BVMemRepr{} _ = LTF
compareF _ BVMemRepr{} = GTF
compareF (FloatMemRepr xf xe) (FloatMemRepr yf ye) =
joinOrderingF (compareF xf yf) $
fromOrdering (compare xe ye)
compareF FloatMemRepr{} _ = LTF
compareF _ FloatMemRepr{} = GTF
compareF (PackedVecMemRepr xn xe) (PackedVecMemRepr yn ye) =
joinOrderingF (compareF xn yn) $
joinOrderingF (compareF xe ye) $
EQF
instance HasRepr MemRepr TypeRepr where
typeRepr (BVMemRepr w _) =
let r = (natMultiply n8 w)
in case leqMulPos (Proxy :: Proxy 8) w of
LeqProof -> BVTypeRepr r
typeRepr (FloatMemRepr f _) = FloatTypeRepr f
typeRepr (PackedVecMemRepr n e) = VecTypeRepr n (typeRepr e)
------------------------------------------------------------------------
-- AssignRhs

10
base/src/Data/Macaw/Types.hs
View File

@ -24,6 +24,7 @@ The type of machine words, including bit vectors and floating point
{-# LANGUAGE UndecidableInstances #-}
module Data.Macaw.Types
( module Data.Macaw.Types -- export everything
, GHC.TypeLits.KnownNat
, GHC.TypeLits.Nat
, Data.Parameterized.NatRepr.NatRepr(..)
, Data.Parameterized.NatRepr.knownNat
@ -77,7 +78,7 @@ n512 = knownNat
-- Floating point sizes
data FloatInfo
= HalfFloat -- ^ 16 bit binary IEE754
= HalfFloat -- ^ 16 bit binary IEE754*
| SingleFloat -- ^ 32 bit binary IEE754
| DoubleFloat -- ^ 64 bit binary IEE754
| QuadFloat -- ^ 128 bit binary IEE754
@ -207,7 +208,7 @@ data TypeRepr (tp :: Type) where
BVTypeRepr :: (1 <= n) => !(NatRepr n) -> TypeRepr (BVType n)
FloatTypeRepr :: !(FloatInfoRepr fi) -> TypeRepr (FloatType fi)
TupleTypeRepr :: !(P.List TypeRepr ctx) -> TypeRepr (TupleType ctx)
VectorTypeRepr :: NatRepr n -> TypeRepr tp -> TypeRepr (VecType n tp)
VecTypeRepr :: NatRepr n -> TypeRepr tp -> TypeRepr (VecType n tp)
type_width :: TypeRepr (BVType n) -> NatRepr n
type_width (BVTypeRepr n) = n
@ -219,7 +220,7 @@ instance Show (TypeRepr tp) where
show (TupleTypeRepr P.Nil) = "()"
show (TupleTypeRepr (h P.:< z)) =
"(" ++ show h ++ foldrFC (\tp r -> "," ++ show tp ++ r) ")" z
show (VectorTypeRepr c tp) = "(vec " ++ show c ++ " " ++ show tp ++ ")"
show (VecTypeRepr c tp) = "(vec " ++ show c ++ " " ++ show tp ++ ")"
instance ShowF TypeRepr
@ -235,6 +236,9 @@ instance (KnownRepr FloatInfoRepr fi) => KnownRepr TypeRepr (FloatType fi) where
instance (KnownRepr (P.List TypeRepr) l) => KnownRepr TypeRepr (TupleType l) where
knownRepr = TupleTypeRepr knownRepr
instance (KnownNat n, KnownRepr TypeRepr r) => KnownRepr TypeRepr (VecType n r) where
knownRepr = VecTypeRepr knownNat knownRepr
$(pure [])
instance TestEquality TypeRepr where

2
deps/crucible vendored

@ -1 +1 @@
Subproject commit 50700454f0d5ba0b0beb23455bd5e27d216bef74
Subproject commit d0c8f1e1a712e779f9995363689b352ce10b17dd

2
deps/flexdis86 vendored

@ -1 +1 @@
Subproject commit 64a3b8154a654e7079a6a5253a00d4fe8dac9934
Subproject commit 0803a143306b70cb33ea70fe758898b1bce5a247

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

@ -4,10 +4,12 @@
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
@ -101,9 +103,10 @@ module Data.Macaw.Symbolic
import GHC.TypeLits
import Control.Lens ((^.))
import Control.Monad (foldM, forM, join)
import Control.Monad
import Control.Monad.IO.Class
import Control.Monad.ST (ST, RealWorld, stToIO)
import Data.Foldable
import qualified Data.Map.Strict as Map
import Data.Maybe
import Data.Parameterized.Context (EmptyCtx, (::>), pattern Empty, pattern (:>))
@ -111,9 +114,11 @@ import qualified Data.Parameterized.Context as Ctx
import Data.Parameterized.Nonce ( NonceGenerator, newSTNonceGenerator )
import Data.Parameterized.Some ( Some(Some) )
import qualified Data.Parameterized.TraversableFC as FC
import qualified Data.Vector as V
import qualified What4.FunctionName as C
import What4.Interface
import What4.InterpretedFloatingPoint as C
import qualified What4.ProgramLoc as C
import What4.Symbol (userSymbol)
@ -135,13 +140,12 @@ import qualified Lang.Crucible.LLVM.MemModel as MM
import Lang.Crucible.LLVM.Intrinsics (llvmIntrinsicTypes)
import qualified Data.Macaw.CFG.Block as M
import qualified Data.Macaw.CFG.Core as M
import qualified Data.Macaw.CFG as M
import qualified Data.Macaw.Discovery.State as M
import qualified Data.Macaw.Memory as M
import qualified Data.Macaw.Types as M
import qualified Data.Macaw.Symbolic.Backend as SB
import Data.Macaw.Symbolic.CrucGen as CG
import Data.Macaw.Symbolic.CrucGen as CG hiding (bvLit)
import Data.Macaw.Symbolic.PersistentState as PS
import Data.Macaw.Symbolic.MemOps as MO
@ -686,7 +690,72 @@ toCoreCFG archFns (CR.SomeCFG cfg) = crucGenArchConstraints archFns $ C.toSSA cf
-- * Symbolic simulation
evalMacawExprExtension :: IsSymInterface sym
plus1LeqDbl :: forall n w . (2 <= n, 1 <= w) => NatRepr n -> NatRepr w -> LeqProof (w+1) (n * w)
plus1LeqDbl n w =
case testLeq (incNat w) (natMultiply n w) of
Nothing -> error "Unexpected vector"
Just p -> p
checkMacawFloatEq :: M.FloatInfoRepr ftp
-> FloatInfoToBitWidth (ToCrucibleFloatInfo ftp) :~: M.FloatInfoBits ftp
checkMacawFloatEq f =
case f of
M.SingleFloatRepr -> Refl
M.HalfFloatRepr -> Refl
M.DoubleFloatRepr -> Refl
M.QuadFloatRepr -> Refl
M.X86_80FloatRepr -> Refl
doBitcast :: forall sym i o
. IsSymInterface sym
=> sym
-> C.RegValue sym (ToCrucibleType i)
-> M.WidthEqProof i o
-> IO (C.RegValue sym (ToCrucibleType o))
doBitcast sym x eqPr =
case eqPr of
M.PackBits (n :: NatRepr n) (w :: NatRepr w) -> do
let outW = natMultiply n w
LeqProof <- pure $ leqMulPos n w
LeqProof <- pure $ plus1LeqDbl n w
when (fromIntegral (V.length x) /= natValue n) $ do
fail "bitcast: Incorrect input vector length"
-- We should have at least one element due to constraint on n
let Just h = x V.!? 0
let rest :: V.Vector (MM.LLVMPtr sym w)
rest = V.tail x
extH <- bvZext sym outW =<< MM.projectLLVM_bv sym h
let doPack :: (Integer,SymBV sym (n*w)) -> MM.LLVMPtr sym w -> IO (Integer, SymBV sym (n*w))
doPack (i,r) y = do
extY <- bvZext sym outW =<< MM.projectLLVM_bv sym y
shiftAmt <- bvLit sym outW i
r' <- bvOrBits sym r =<< bvShl sym extY shiftAmt
pure (i+1,r')
(_,r) <- foldlM doPack (1,extH) rest
MM.llvmPointer_bv sym r
M.UnpackBits n w -> do
let inW = natMultiply n w
LeqProof <- pure $ leqMulPos n w
LeqProof <- pure $ plus1LeqDbl n w
xbv <- MM.projectLLVM_bv sym x
V.generateM (fromIntegral (natValue n)) $ \i -> do
shiftAmt <- bvLit sym inW (toInteger i)
MM.llvmPointer_bv sym =<< bvTrunc sym w =<< bvLshr sym xbv shiftAmt
M.FromFloat f -> do
Refl <- pure $ checkMacawFloatEq f
xbv <- C.iFloatToBinary sym (floatInfoToCrucible f) x
MM.llvmPointer_bv sym xbv
M.ToFloat f -> do
xbv <- MM.projectLLVM_bv sym x
Refl <- pure $ checkMacawFloatEq f
C.iFloatFromBinary sym (floatInfoToCrucible f) xbv
M.VecEqCongruence _n eltPr -> do
forM x $ \e -> doBitcast sym e eltPr
evalMacawExprExtension :: forall sym arch f tp
. IsSymInterface sym
=> sym
-> C.IntrinsicTypes sym
-> (Int -> String -> IO ())
@ -730,11 +799,13 @@ evalMacawExprExtension sym _iTypes _logFn f e0 =
znorm <- bvSext sym w' =<< bvTrunc sym w zext
bvNe sym zext znorm
PtrToBits w x -> doPtrToBits sym w =<< f x
PtrToBits _w x -> doPtrToBits sym =<< f x
BitsToPtr _w x -> MM.llvmPointer_bv sym =<< f x
MacawNullPtr w | LeqProof <- addrWidthIsPos w -> MM.mkNullPointer sym (M.addrWidthNatRepr w)
MacawBitcast xExpr eqPr -> do
x <- f xExpr
doBitcast sym x eqPr
-- | This evaluates a Macaw statement extension in the simulator.
execMacawStmtExtension
@ -747,15 +818,29 @@ execMacawStmtExtension
-> MO.GlobalMap sym (M.ArchAddrWidth arch)
-- ^ The translation from machine words to LLVM memory model pointers
-> MO.LookupFunctionHandle sym arch
-- ^ A function to turn machine addresses into Crucible function handles (which can also perform lazy CFG creation)
-- ^ A function to turn machine addresses into Crucible function
-- handles (which can also perform lazy CFG creation)
-> SB.EvalStmtFunc (MacawStmtExtension arch) (MacawSimulatorState sym) sym (MacawExt arch)
execMacawStmtExtension (SB.MacawArchEvalFn archStmtFn) mvar globs (MO.LookupFunctionHandle lookupH) s0 st =
case s0 of
MacawReadMem w mr x -> doReadMem st mvar globs w mr x
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
MacawGlobalPtr w addr -> M.addrWidthClass w $ doGetGlobal st mvar globs addr
MacawReadMem addrWidth memRep ptr0 -> do
let sym = st^.C.stateSymInterface
mem <- getMem st mvar
ptr <- tryGlobPtr sym mem globs (C.regValue ptr0)
(,st) <$> doReadMem sym mem addrWidth memRep ptr
MacawCondReadMem addrWidth memRep cond ptr0 condFalseValue -> do
let sym = st^.C.stateSymInterface
mem <- getMem st mvar
ptr <- tryGlobPtr sym mem globs (C.regValue ptr0)
(,st) <$> doCondReadMem sym mem addrWidth memRep (C.regValue cond) ptr (C.regValue condFalseValue)
MacawWriteMem addrWidth memRep ptr0 v -> do
let sym = st^.C.stateSymInterface
mem <- getMem st mvar
ptr <- tryGlobPtr sym mem globs (C.regValue ptr0)
mem1 <- doWriteMem sym mem addrWidth memRep ptr (C.regValue v)
pure ((), setMem st mvar mem1)
MacawGlobalPtr w addr ->
M.addrWidthClass w $ doGetGlobal st mvar globs addr
MacawFreshSymbolic t -> -- XXX: user freshValue
do nm <- case userSymbol "macawFresh" of

3
symbolic/src/Data/Macaw/Symbolic/Backend.hs
View File

@ -30,6 +30,9 @@ module Data.Macaw.Symbolic.Backend (
, MO.doGetGlobal
, MO.doLookupFunctionHandle
, MO.doPtrToBits
, MO.getMem
, MO.setMem
, MO.tryGlobPtr
-- ** Register Mapping
, PS.RegIndexMap
, PS.mkRegIndexMap

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

@ -236,7 +236,6 @@ data MacawOverflowOp
deriving (Eq, Ord, Show)
type BVPtr a = MM.LLVMPointerType (M.ArchAddrWidth a)
type ArchNatRepr a = NatRepr (M.ArchAddrWidth a)
-- | The extra expressions required to extend Crucible to support simulating
-- Macaw programs
@ -267,17 +266,23 @@ data MacawExprExtension (arch :: *)
-- pointer. The simulator will attempt the conversion with
-- 'MM.llvmPointer_bv', which generates side conditions that will be tested by
-- the solver.
BitsToPtr ::
(1 <= w) =>
!(NatRepr w) ->
!(f (C.BVType w)) ->
MacawExprExtension arch f (MM.LLVMPointerType w)
BitsToPtr
:: (1 <= w)
=> !(NatRepr w)
-> !(f (C.BVType w))
-> MacawExprExtension arch f (MM.LLVMPointerType w)
-- | A null pointer.
MacawNullPtr
:: !(ArchAddrWidthRepr arch)
-> MacawExprExtension arch f (BVPtr arch)
-- | Cast from one macaw value to another.
MacawBitcast :: !(f (ToCrucibleType i))
-> !(M.WidthEqProof i o)
-> MacawExprExtension arch f (ToCrucibleType o)
instance C.PrettyApp (MacawExprExtension arch) where
ppApp f a0 =
case a0 of
@ -289,6 +294,7 @@ instance C.PrettyApp (MacawExprExtension arch) where
BitsToPtr w x -> sexpr ("bits_to_ptr_" ++ show w) [f x]
MacawNullPtr _ -> sexpr "null_ptr" []
MacawBitcast x p -> sexpr "bitcast" [f x, text (show (M.widthEqTarget p))]
addrWidthIsPos :: M.AddrWidthRepr w -> LeqProof 1 w
addrWidthIsPos M.Addr32 = LeqProof
@ -301,7 +307,7 @@ instance C.TypeApp (MacawExprExtension arch) where
PtrToBits w _ -> C.BVRepr w
BitsToPtr w _ -> MM.LLVMPointerRepr w
MacawNullPtr w | LeqProof <- addrWidthIsPos w -> MM.LLVMPointerRepr (M.addrWidthNatRepr w)
MacawBitcast _ p -> typeToCrucible (M.widthEqTarget p)
------------------------------------------------------------------------
-- MacawStmtExtension
@ -319,16 +325,13 @@ data MacawStmtExtension (arch :: *)
-- | Read from memory.
--
-- The 'M.MemRepr' describes the endianness and size of the read.
MacawReadMem ::
!(ArchAddrWidthRepr arch) ->
MacawReadMem
:: !(ArchAddrWidthRepr arch)
-- Info about memory (endianness, size)
!(M.MemRepr tp) ->
-> !(M.MemRepr tp)
-- Pointer to read from.
!(f (ArchAddrCrucibleType arch)) ->
MacawStmtExtension arch f (ToCrucibleType tp)
-> !(f (ArchAddrCrucibleType arch))
-> MacawStmtExtension arch f (ToCrucibleType tp)
-- | Read from memory, if the condition is True.
@ -375,9 +378,11 @@ data MacawStmtExtension (arch :: *)
--
-- This needs to be a statement to support the dynamic translation of the
-- target CFG, and especially the registration of that CFG with the simulator.
MacawLookupFunctionHandle :: !(Assignment C.TypeRepr (CtxToCrucibleType (ArchRegContext arch)))
-> !(f (ArchRegStruct arch))
-> MacawStmtExtension arch f (C.FunctionHandleType (Ctx.EmptyCtx Ctx.::> ArchRegStruct arch) (ArchRegStruct arch))
MacawLookupFunctionHandle
:: !(Assignment C.TypeRepr (CtxToCrucibleType (ArchRegContext arch)))
-> !(f (ArchRegStruct arch))
-> MacawStmtExtension arch f (C.FunctionHandleType (Ctx.EmptyCtx Ctx.::> ArchRegStruct arch)
(ArchRegStruct arch))
-- | An architecture-specific machine instruction, for which an interpretation
-- is required. This interpretation must be provided by callers via the
@ -409,58 +414,56 @@ data MacawStmtExtension (arch :: *)
-- inputs are valid pointers.
-- | Equality for pointer or bit-vector.
PtrEq ::
!(ArchAddrWidthRepr arch) ->
!(f (BVPtr arch)) ->
!(f (BVPtr arch)) ->
MacawStmtExtension arch f C.BoolType
PtrEq
:: !(ArchAddrWidthRepr arch)
-> !(f (BVPtr arch))
-> !(f (BVPtr arch))
-> MacawStmtExtension arch f C.BoolType
-- | Unsigned comparison for pointer/bit-vector.
PtrLeq ::
!(ArchAddrWidthRepr arch) ->
!(f (BVPtr arch)) ->
!(f (BVPtr arch)) ->
MacawStmtExtension arch f C.BoolType
PtrLeq
:: !(ArchAddrWidthRepr arch)
-> !(f (BVPtr arch))
-> !(f (BVPtr arch))
-> MacawStmtExtension arch f C.BoolType
-- | Unsigned comparison for pointer/bit-vector.
PtrLt ::
!(ArchAddrWidthRepr arch) ->
!(f (BVPtr arch)) ->
!(f (BVPtr arch)) ->
MacawStmtExtension arch f C.BoolType
PtrLt
:: !(ArchAddrWidthRepr arch)
-> !(f (BVPtr arch))
-> !(f (BVPtr arch))
-> MacawStmtExtension arch f C.BoolType
-- | Mux for pointers or bit-vectors.
PtrMux ::
!(ArchAddrWidthRepr arch) ->
!(f C.BoolType) ->
!(f (BVPtr arch)) ->
!(f (BVPtr arch)) ->
MacawStmtExtension arch f (BVPtr arch)
PtrMux
:: !(ArchAddrWidthRepr arch)
-> !(f C.BoolType)
-> !(f (BVPtr arch))
-> !(f (BVPtr arch))
-> MacawStmtExtension arch f (BVPtr arch)
-- | Add a pointer to a bit-vector, or two bit-vectors.
PtrAdd ::
!(ArchAddrWidthRepr arch) ->
!(f (BVPtr arch)) ->
!(f (BVPtr arch)) ->
MacawStmtExtension arch f (BVPtr arch)
PtrAdd
:: !(ArchAddrWidthRepr arch)
-> !(f (BVPtr arch))
-> !(f (BVPtr arch))
-> MacawStmtExtension arch f (BVPtr arch)
-- | Subtract two pointers, two bit-vectors, or bit-vector from a pointer.
PtrSub ::
!(ArchAddrWidthRepr arch) ->
!(f (BVPtr arch)) ->
!(f (BVPtr arch)) ->
MacawStmtExtension arch f (BVPtr arch)
PtrSub
:: !(ArchAddrWidthRepr arch)
-> !(f (BVPtr arch))
-> !(f (BVPtr arch))
-> MacawStmtExtension arch f (BVPtr arch)
-- | And together two items. Usually these are going to be bit-vectors,
-- but sometimes we need to support "and"-ing a pointer with a constant,
-- which happens when trying to align a pointer.
PtrAnd ::
!(ArchAddrWidthRepr arch) ->
!(f (BVPtr arch)) ->
!(f (BVPtr arch)) ->
MacawStmtExtension arch f (BVPtr arch)
PtrAnd
:: !(ArchAddrWidthRepr arch)
-> !(f (BVPtr arch))
-> !(f (BVPtr arch))
-> MacawStmtExtension arch f (BVPtr arch)
instance TraversableFC (MacawArchStmtExtension arch)
=> FunctorFC (MacawStmtExtension arch) where
@ -478,7 +481,9 @@ instance (C.PrettyApp (MacawArchStmtExtension arch),
M.PrettyF (M.ArchReg arch),
M.MemWidth (M.RegAddrWidth (M.ArchReg arch)))
=> C.PrettyApp (MacawStmtExtension arch) where
ppApp :: forall f . (forall (x :: C.CrucibleType) . f x -> Doc) -> (forall (x :: C.CrucibleType) . MacawStmtExtension arch f x -> Doc)
ppApp :: forall f
. (forall (x :: C.CrucibleType) . f x -> Doc)
-> (forall (x :: C.CrucibleType) . MacawStmtExtension arch f x -> Doc)
ppApp f a0 =
case a0 of
MacawReadMem _ r a -> sexpr "macawReadMem" [pretty r, f a]
@ -513,7 +518,8 @@ instance C.TypeApp (MacawArchStmtExtension arch)
appType (MacawGlobalPtr w _)
| LeqProof <- addrWidthIsPos w = MM.LLVMPointerRepr (M.addrWidthNatRepr w)
appType (MacawFreshSymbolic r) = typeToCrucible r
appType (MacawLookupFunctionHandle regTypes _) = C.FunctionHandleRepr (Ctx.singleton (C.StructRepr regTypes)) (C.StructRepr regTypes)
appType (MacawLookupFunctionHandle regTypes _) =
C.FunctionHandleRepr (Ctx.singleton (C.StructRepr regTypes)) (C.StructRepr regTypes)
appType (MacawArchStmtExtension f) = C.appType f
appType MacawArchStateUpdate {} = C.knownRepr
appType MacawInstructionStart {} = C.knownRepr
@ -827,21 +833,17 @@ addLemma x y =
bvLit :: (1 <= w) => NatRepr w -> Integer -> CrucGen arch ids h s (CR.Atom s (C.BVType w))
bvLit w i = crucibleValue (C.BVLit w (i .&. maxUnsigned w))
bitOp2 ::
(1 <= w) =>
NatRepr w ->
(CR.Atom s (C.BVType w) ->
CR.Atom s (C.BVType w) ->
C.App (MacawExt arch) (CR.Atom s) (C.BVType w)) ->
M.Value arch ids (M.BVType w) ->
M.Value arch ids (M.BVType w) ->
CrucGen arch ids h s (CR.Atom s (MM.LLVMPointerType w))
bitOp2 :: (1 <= w)
=> NatRepr w
-> (CR.Atom s (C.BVType w)
-> CR.Atom s (C.BVType w)
-> C.App (MacawExt arch) (CR.Atom s) (C.BVType w))
-> M.Value arch ids (M.BVType w)
-> M.Value arch ids (M.BVType w)
-> CrucGen arch ids h s (CR.Atom s (MM.LLVMPointerType w))
bitOp2 w f x y = fromBits w =<< appAtom =<< f <$> v2c' w x <*> v2c' w y
appToCrucible
:: forall arch ids h s tp
. M.App (M.Value arch ids) tp
@ -864,23 +866,25 @@ appToCrucible app = do
appAtom =<< C.BVEq n <$> toBits n xv <*> toBits n yv
M.FloatTypeRepr _ -> appAtom $ C.FloatEq xv yv
M.TupleTypeRepr _ -> fail "XXX: Equality on tuples not yet done."
M.VecTypeRepr{} -> fail "XXX: Equality on vectors not yet done."
M.Mux tp c t f ->
do cond <- v2c c
tv <- v2c t
fv <- v2c f
case tp of
M.BoolTypeRepr -> appAtom (C.BaseIte C.BaseBoolRepr cond tv fv)
M.BVTypeRepr n ->
M.Mux tp c t f -> do
cond <- v2c c
tv <- v2c t
fv <- v2c f
case tp of
M.BoolTypeRepr -> appAtom (C.BaseIte C.BaseBoolRepr cond tv fv)
M.BVTypeRepr n ->
do rW <- archAddrWidth
case testEquality n (M.addrWidthNatRepr rW) of
Just Refl -> evalMacawStmt (PtrMux rW cond tv fv)
Nothing -> appBVAtom n =<<
C.BVIte cond n <$> toBits n tv <*> toBits n fv
M.FloatTypeRepr fi ->
M.FloatTypeRepr fi ->
appAtom $ C.FloatIte (floatInfoToCrucible fi) cond tv fv
M.TupleTypeRepr _ -> fail "XXX: Mux on tuples not yet done."
M.TupleTypeRepr _ -> fail "XXX: Mux on tuples not yet done."
M.VecTypeRepr{} -> fail "XXX: Mux on vectors not yet done."
M.TupleField tps x i -> do
@ -901,27 +905,31 @@ appToCrucible app = do
M.XorApp x y -> appAtom =<< C.BoolXor <$> v2c x <*> v2c y
-- Extension operations
M.Trunc x w ->
do let wx = M.typeWidth x
LeqProof <- return (addLemma w wx)
appBVAtom w =<< C.BVTrunc w wx <$> v2c' wx x
M.Trunc x w -> do
let wx = M.typeWidth x
LeqProof <- return (addLemma w wx)
appBVAtom w =<< C.BVTrunc w wx <$> v2c' wx x
M.SExt x w ->
do let wx = M.typeWidth x
appBVAtom w =<< C.BVSext w wx <$> v2c' wx x
M.SExt x w -> do
let wx = M.typeWidth x
appBVAtom w =<< C.BVSext w wx <$> v2c' wx x
M.UExt x w ->
do let wx = M.typeWidth x
appBVAtom w =<< C.BVZext w wx <$> v2c' wx x
M.UExt x w -> do
let wx = M.typeWidth x
appBVAtom w =<< C.BVZext w wx <$> v2c' wx x
M.Bitcast v p -> do
crucValue <- v2c v
evalMacawExt (MacawBitcast crucValue p)
-- Bitvector arithmetic
M.BVAdd w x y ->
do xv <- v2c x
yv <- v2c y
aw <- archAddrWidth
case testEquality w (M.addrWidthNatRepr aw) of
Just Refl -> evalMacawStmt (PtrAdd aw xv yv)
Nothing -> appBVAtom w =<< C.BVAdd w <$> toBits w xv <*> toBits w yv
M.BVAdd w x y -> do
xv <- v2c x
yv <- v2c y
aw <- archAddrWidth
case testEquality w (M.addrWidthNatRepr aw) of
Just Refl -> evalMacawStmt (PtrAdd aw xv yv)
Nothing -> appBVAtom w =<< C.BVAdd w <$> toBits w xv <*> toBits w yv
-- Here we assume that this does not make sense for pointers.
M.BVAdc w x y c -> do
@ -931,13 +939,13 @@ appToCrucible app = do
<*> appAtom (C.BVLit w 0)
appBVAtom w (C.BVAdd w z d)
M.BVSub w x y ->
do xv <- v2c x
yv <- v2c y
aw <- archAddrWidth
case testEquality w (M.addrWidthNatRepr aw) of
Just Refl -> evalMacawStmt (PtrSub aw xv yv)
Nothing -> appBVAtom w =<< C.BVSub w <$> toBits w xv <*> toBits w yv
M.BVSub w x y -> do
xv <- v2c x
yv <- v2c y
aw <- archAddrWidth
case testEquality w (M.addrWidthNatRepr aw) of
Just Refl -> evalMacawStmt (PtrSub aw xv yv)
Nothing -> appBVAtom w =<< C.BVSub w <$> toBits w xv <*> toBits w yv
M.BVSbb w x y c -> do
z <- appAtom =<< C.BVSub w <$> v2c' w x <*> v2c' w y
@ -1593,18 +1601,22 @@ $(return [])
instance TestEqualityFC (MacawExprExtension arch) where
testEqualityFC f =
$(U.structuralTypeEquality [t|MacawExprExtension|]
[ (U.DataArg 1 `U.TypeApp` U.AnyType, [|f|])
, (U.ConType [t|NatRepr |] `U.TypeApp` U.AnyType, [|testEquality|])
[ (U.DataArg 1 `U.TypeApp` U.AnyType, [|f|])
, (U.ConType [t|NatRepr |] `U.TypeApp` U.AnyType, [|testEquality|])
, (U.ConType [t|ArchAddrWidthRepr|] `U.TypeApp` U.AnyType, [|testEquality|])
, (U.ConType [t|M.WidthEqProof|] `U.TypeApp` U.AnyType `U.TypeApp` U.AnyType,
[|M.widthEqProofEq|])
])
instance OrdFC (MacawExprExtension arch) where
compareFC f =
$(U.structuralTypeOrd [t|MacawExprExtension|]
[ (U.DataArg 1 `U.TypeApp` U.AnyType, [|f|])
, (U.ConType [t|NatRepr|] `U.TypeApp` U.AnyType, [|compareF|])
, (U.ConType [t|ArchNatRepr|] `U.TypeApp` U.AnyType, [|compareF|])
, (U.ConType [t|ArchAddrWidthRepr|] `U.TypeApp` U.AnyType, [|compareF|])
[ (U.DataArg 1 `U.TypeApp` U.AnyType, [|f|])
, (U.ConType [t|NatRepr|] `U.TypeApp` U.AnyType, [|compareF|])
, (U.ConType [t|ArchAddrWidthRepr|] `U.TypeApp` U.AnyType, [|compareF|])
, (U.ConType [t|M.WidthEqProof|] `U.TypeApp` U.AnyType `U.TypeApp` U.AnyType,
[|M.widthEqProofCompare|])
])
instance FunctorFC (MacawExprExtension arch) where

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

@ -2,6 +2,7 @@
-- depending on if they are applied to pointers or bit-vectors.
{-# LANGUAGE ConstraintKinds #-}
{-# Language DataKinds #-}
{-# Language FlexibleContexts #-}
{-# Language TypeOperators #-}
{-# Language TypeFamilies #-}
{-# Language ImplicitParams #-}
@ -25,15 +26,20 @@ module Data.Macaw.Symbolic.MemOps
, doGetGlobal
, doLookupFunctionHandle
, doPtrToBits
, getMem
, setMem
, tryGlobPtr
, Regs
, MacawSimulatorState(..)
, LookupFunctionHandle(..)
) where
import Control.Exception (throwIO)
import Control.Lens ((^.),(&),(%~))
import Control.Monad (guard)
import Control.Monad (guard, when)
import Data.Bits (testBit)
import Data.Maybe ( fromMaybe )
import qualified Data.Vector as V
import Data.Parameterized (Some(..))
import qualified Data.Parameterized.Context as Ctx
@ -60,25 +66,31 @@ import Lang.Crucible.Types
import Lang.Crucible.LLVM.MemModel
( Mem, MemImpl, LLVMPointerType, LLVMPtr, isValidPointer, memEndian
, LLVMVal(LLVMValInt)
, loadRaw
, loadRawWithCondition
, storeRaw
, llvmPointerView, muxLLVMPtr, llvmPointer_bv, ptrAdd, ptrSub, ptrEq
, pattern LLVMPointer
, mkNullPointer
, bitvectorType
, ppPtr
, ptrMessage
)
import qualified Lang.Crucible.LLVM.MemModel as Mem
import Lang.Crucible.LLVM.DataLayout (EndianForm(..), noAlignment)
import Lang.Crucible.LLVM.Bytes (toBytes)
import Lang.Crucible.LLVM.Bytes (Bytes(..))
import Data.Macaw.Symbolic.CrucGen (addrWidthIsPos, ArchRegStruct, MacawExt, MacawCrucibleRegTypes)
import Data.Macaw.Symbolic.PersistentState (ToCrucibleType)
import Data.Macaw.CFG.Core (MemRepr(BVMemRepr))
import Data.Macaw.CFG.Core (MemRepr(..))
import qualified Data.Macaw.CFG as M
infix 0 ~>
(~>) :: a -> b -> (a,b)
x ~> y = (x,y)
-- | The offset part of a pointer.
asBits :: LLVMPtr sym w -> RegValue sym (BVType w)
asBits = snd . llvmPointerView
-- | The base part of a point.
ptrBase :: LLVMPtr sym w -> RegValue sym NatType
ptrBase = fst . llvmPointerView
-- | The 'GlobalMap' is a function that maps from (possibly segmented) program
-- virtual addresses into pointers into the LLVM memory model heap (the
-- 'LLVMPtr' type).
@ -133,25 +145,142 @@ import qualified Data.Macaw.CFG as M
-- contains the relocatable value, and 2) returning the corresponding address in
-- that allocation.
type GlobalMap sym w = sym {-^ The symbolic backend -} ->
RegValue sym Mem {-^ The global handle to the memory model -} ->
MemImpl sym {-^ The global handle to the memory model -} ->
RegValue sym NatType {-^ The region index of the pointer being translated -} ->
RegValue sym (BVType w) {-^ The offset of the pointer into the region -} ->
IO (Maybe (LLVMPtr sym w))
{- | Every now and then we encounter memory opperations that
just read/write to some constant. Normally, we do not allow
such things as we want memory to be allocated first.
However we need to make an exception for globals.
So, if we ever try to manipulate memory at some address
which is statically known to be a constant, we consult
the global map to see if we know about a correpsonding
address. If so, we use that for the memory operation.
See the documentation of 'GlobalMap' for details about how that translation can
be handled.
-}
tryGlobPtr ::
IsSymInterface sym =>
sym ->
RegValue sym Mem ->
GlobalMap sym w ->
LLVMPtr sym w ->
IO (LLVMPtr sym w)
tryGlobPtr sym mem mapBVAddress val
| Just 0 <- asNat (ptrBase val) = do
maddr <- mapBVAddress sym mem (ptrBase val) (asBits val)
return (fromMaybe val maddr)
| otherwise = return val
-- | This is the form of binary operation needed by the simulator.
-- Note that even though the type suggests that we might modify the
-- state, we don't actually do it.
type PtrOp sym w a =
forall s ext rtp blocks r ctx.
IsSymInterface sym =>
CrucibleState s sym ext rtp blocks r ctx {- ^ Simulator state -} ->
GlobalVar Mem {- ^ Memory model -} ->
M.AddrWidthRepr w {- ^ Width of pointer -} ->
RegEntry sym (LLVMPointerType w) {- ^ Argument 1 -} ->
RegEntry sym (LLVMPointerType w) {- ^ Argument 2 -} ->
IO (a, CrucibleState s sym ext rtp blocks r ctx)
-- | Get the current model of the memory.
getMem :: CrucibleState s sym ext rtp blocks r ctx ->
GlobalVar Mem ->
IO (MemImpl sym)
getMem st mvar =
case lookupGlobal mvar (st ^. stateTree . actFrame . gpGlobals) of
Just mem -> return mem
Nothing -> fail ("Global heap value not initialized: " ++ show mvar)
setMem :: CrucibleState s sym ext rtp blocks r ctx ->
GlobalVar Mem ->
MemImpl sym ->
CrucibleState s sym ext rtp blocks r ctx
setMem st mvar mem =
st & stateTree . actFrame . gpGlobals %~ insertGlobal mvar mem
-- | Classify the arguments, and continue.
ptrOp ::
( (1 <= w) =>
sym ->
RegValue sym Mem ->
M.AddrWidthRepr w ->
Pred sym -> Pred sym -> Pred sym -> Pred sym ->
LLVMPtr sym w -> LLVMPtr sym w -> IO a
) ->
PtrOp sym w a
ptrOp k st mvar w x0 y0 =
do mem <- getMem st mvar
LeqProof <- return (addrWidthIsPos w)
let sym = st^.stateSymInterface
x = regValue x0
y = regValue y0
zero <- natLit sym 0
xBits <- natEq sym (ptrBase x) zero
xPtr <- notPred sym xBits
yBits <- natEq sym (ptrBase y) zero
yPtr <- notPred sym yBits
a <- k sym mem w xPtr xBits yPtr yBits x y
return (a,st)
mkName :: String -> IO SolverSymbol
mkName x = case userSymbol x of
Right v -> return v
Left err ->
fail $ unlines
[ "[bug] " ++ show x ++ " is not a valid identifier?"
, "*** " ++ show err
]
mkUndefined ::
(IsSymInterface sym) =>
sym -> String -> BaseTypeRepr t -> IO (RegValue sym (BaseToType t))
mkUndefined sym unm ty =
do let name = "undefined_" ++ unm
nm <- mkName name
freshConstant sym nm ty
-- | A fresh bit-vector variable
mkUndefinedBV ::
(IsSymInterface sym, 1 <= w) =>
sym -> String -> NatRepr w -> IO (RegValue sym (BVType w))
mkUndefinedBV sym nm w =
mkUndefined sym (nm ++ "bv" ++ show w ++ "_") (BaseBVRepr w)
-- | A fresh boolean variable
mkUndefinedBool ::
(IsSymInterface sym) => sym -> String -> IO (RegValue sym BoolType)
mkUndefinedBool sym nm =
mkUndefined sym (nm ++ "bool_") BaseBoolRepr
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 (Mem.LLVMPointer base off)
-- | This is called whenever a (bit-vector/pointer) is used as a bit-vector.
-- The result is undefined (i.e., a fresh unknown value) if it is given
-- a real pointer.
doPtrToBits ::
(IsSymInterface sym, 1 <= w) =>
sym ->
NatRepr w ->
LLVMPtr sym w ->
IO (RegValue sym (BVType w))
doPtrToBits sym w p =
do let base = ptrBase p
undef <- mkUndefinedBV sym "ptr_to_bits" w
IO (SymBV sym w)
doPtrToBits sym (Mem.LLVMPointer base off) =
do undef <- mkUndefinedBV sym "ptr_to_bits" (bvWidth off)
notPtr <- natEq sym base =<< natLit sym 0
bvIte sym notPtr (asBits p) undef
bvIte sym notPtr off undef
-- | The state extension for Crucible holding Macaw-specific state
--
@ -224,34 +353,78 @@ doGetGlobal st mvar globs addr = do
--------------------------------------------------------------------------------
-- | This is the form of binary operation needed by the simulator.
-- Note that even though the type suggests that we might modify the
-- state, we don't actually do it.
type PtrOp sym w a =
forall s ext rtp blocks r ctx.
IsSymInterface sym =>
CrucibleState s sym ext rtp blocks r ctx {- ^ Simulator state -} ->
GlobalVar Mem {- ^ Memory model -} ->
M.AddrWidthRepr w {- ^ Width of pointer -} ->
RegEntry sym (LLVMPointerType w) {- ^ Argument 1 -} ->
RegEntry sym (LLVMPointerType w) {- ^ Argument 2 -} ->
IO (a, CrucibleState s sym ext rtp blocks r ctx)
binOpLabel :: IsSymInterface sym =>
String -> LLVMPtr sym w -> LLVMPtr sym w -> String
binOpLabel lab x y =
unlines [ "{ instruction: " ++ lab
, ", operand 1: " ++ show (ppPtr x)
, ", operand 2: " ++ show (ppPtr y)
, ", operand 1: " ++ show (Mem.ppPtr x)
, ", operand 2: " ++ show (Mem.ppPtr 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)
check :: IsSymInterface sym => sym -> Pred sym -> String -> String -> IO ()
check sym valid name msg = assert sym valid
$ AssertFailureSimError
$ "[" ++ name ++ "] " ++ msg
-- | Define an operation by cases.
cases ::
(IsSymInterface sym) =>
sym {- ^ Simulator -} ->
String {- ^ Name of operation (for assertions) -} ->
(sym -> Pred sym -> a -> a -> IO a) {- Mux results -} ->
Maybe a {- ^ Default: use this if none of the cases matched -} ->
[(Pred sym, IO ([(Pred sym,String)], a))]
{- ^ Cases: (predicate when valid, result + additional checks) -} ->
IO a
cases sym name mux def opts =
case def of
Just _ -> combine =<< mapM doCase opts
Nothing ->
do ok <- oneOf (map fst opts)
check sym ok name ("Invalid arguments for " ++ show name)
combine =<< mapM doCase opts
where
oneOf xs =
case xs of
[] -> return (falsePred sym) -- shouldn't happen
[p] -> return p
p : ps -> orPred sym p =<< oneOf ps
combine [] = fail "[bug] Empty cases"
combine [(p,a)] = case def of
Just d -> mux sym p a d
Nothing -> return a
combine ((p,a) : more) = mux sym p a =<< combine more
doCase (p,m) =
do (checks,a) <- m
mapM_ (subCheck p) checks
return (p,a)
subCheck cp (p,msg) =
do valid <- impliesPred sym cp p
check sym valid name msg
endCase :: Monad m => a -> m ([b],a)
endCase r = return ([],r)
endCaseCheck :: Monad m => a -> b -> c -> m ([(a,b)],c)
endCaseCheck a b c = return ([(a,b)],c)
isValidPtr ::
(IsSymInterface sym) =>
sym ->
MemImpl sym ->
M.AddrWidthRepr w ->
LLVMPtr sym w ->
IO (Pred sym)
isValidPtr sym mem w p =
do LeqProof <- pure $ addrWidthIsPos w
LeqProof <- pure $ addrWidthAtLeast16 w
let ?ptrWidth = M.addrWidthNatRepr w
isValidPointer sym p mem
doPtrMux :: Pred sym -> PtrOp sym w (LLVMPtr sym w)
doPtrMux c = ptrOp $ \sym _ w xPtr xBits yPtr yBits x y ->
@ -280,19 +453,6 @@ doPtrAdd = ptrOp $ \sym _ w xPtr xBits yPtr yBits x y ->
]
return a
isValidPtr ::
(IsSymInterface sym) =>
sym ->
RegValue sym Mem ->
M.AddrWidthRepr w ->
LLVMPtr sym w ->
IO (Pred sym)
isValidPtr sym mem w p =
do LeqProof <- pure $ addrWidthIsPos w
LeqProof <- pure $ addrWidthAtLeast16 w
let ?ptrWidth = M.addrWidthNatRepr w
isValidPointer sym p mem
doPtrSub :: PtrOp sym w (LLVMPtr sym w)
doPtrSub = ptrOp $ \sym mem w xPtr xBits yPtr yBits x y ->
do both_bits <- andPred sym xBits yBits
@ -315,12 +475,22 @@ doPtrSub = ptrOp $ \sym mem w xPtr xBits yPtr yBits x y ->
endCaseCheck ok "Pointers in different regions" r
]
isAlignMask :: (IsSymInterface sym) => LLVMPtr sym w -> Maybe Integer
isAlignMask v =
do 0 <- asNat (ptrBase v)
let off = asBits v
w = fromInteger (intValue (bvWidth off))
k <- asUnsignedBV off
let (zeros,ones) = break (testBit k) (take w [ 0 .. ])
guard (all (testBit k) ones)
return (fromIntegral (length zeros))
doPtrAnd :: PtrOp sym w (LLVMPtr sym w)
doPtrAnd = ptrOp $ \sym _mem w xPtr xBits yPtr yBits x y ->
let nw = M.addrWidthNatRepr w
doPtrAlign amt isP isB v
| amt == 0 = return v
| amt == intValue nw = mkNullPointer sym nw
| amt == intValue nw = Mem.mkNullPointer sym nw
| Just 0 <- asNat (ptrBase v) = llvmPointer_bv sym =<<
bvAndBits sym (asBits x) (asBits y)
@ -352,8 +522,8 @@ doPtrAnd = ptrOp $ \sym _mem w xPtr xBits yPtr yBits x y ->
in case (isAlignMask x, isAlignMask y) of
(Just yes, _) -> doPtrAlign yes yPtr yBits y
(_, Just yes) -> doPtrAlign yes xPtr xBits x
_ -> do v1 <- doPtrToBits sym nw x
v2 <- doPtrToBits sym nw y
_ -> do v1 <- doPtrToBits sym x
v2 <- doPtrToBits sym y
llvmPointer_bv sym =<< bvAndBits sym v1 v2
@ -402,335 +572,225 @@ doPtrEq = ptrOp $ \sym mem w xPtr xBits yPtr yBits x y ->
endCaseCheck ok "Comparing invalid pointers" ps
]
getEnd :: MemImpl sym -> M.Endianness
getEnd mem =
case memEndian mem of
BigEndian -> M.BigEndian
LittleEndian -> M.LittleEndian
checkEndian :: M.Endianness -> M.Endianness -> Either String ()
checkEndian have need =
when (need /= have) $ Left $
unlines [ "[doReadMem] Endian mismatch:"
, " *** Model: " ++ show have
, " *** Read : " ++ show need
]
-- | Convert a mem repr to a memory model storage type. May return an
-- error message if the mem repr is not supported.
memReprToStorageType :: M.Endianness -- ^ Expected endianness of arguments.
-> MemRepr ty
-> Either String Mem.StorageType
memReprToStorageType reqEnd memRep =
case memRep of
M.BVMemRepr bytes endian -> do
checkEndian reqEnd endian
pure $ Mem.bitvectorType (Bytes (intValue bytes))
M.FloatMemRepr floatRep endian -> do
checkEndian reqEnd endian
case floatRep of
M.SingleFloatRepr -> pure Mem.floatType
M.DoubleFloatRepr -> pure Mem.doubleType
M.X86_80FloatRepr -> pure Mem.x86_fp80Type
_ -> Left $ "Do not support memory accesses to " ++ show floatRep ++ " values."
M.PackedVecMemRepr n eltType -> do
eltStorageType <- memReprToStorageType reqEnd eltType
pure $ Mem.arrayType (Bytes (intValue n)) eltStorageType
-- | Convert a Crucible register value to a LLVM memory mode lvalue
resolveMemVal :: MemRepr ty -> -- ^ What/how we are writing
Mem.StorageType -> -- ^ Previously computed storage type for value
RegValue sym (ToCrucibleType ty) -> -- ^ Value to write
Mem.LLVMVal sym
resolveMemVal (M.BVMemRepr bytes _endian) _ (Mem.LLVMPointer base bits) =
case leqMulPos (knownNat @8) bytes of
LeqProof -> Mem.LLVMValInt base bits
resolveMemVal (M.FloatMemRepr floatRep _endian) _ val =
case floatRep of
M.SingleFloatRepr -> Mem.LLVMValFloat Mem.SingleSize val
M.DoubleFloatRepr -> Mem.LLVMValFloat Mem.DoubleSize val
M.X86_80FloatRepr -> Mem.LLVMValFloat Mem.X86_FP80Size val
_ -> error $ "Do not support memory accesses to " ++ show floatRep ++ " values."
resolveMemVal (M.PackedVecMemRepr n eltType) stp val =
case Mem.storageTypeF stp of
Mem.Array cnt eltStp | cnt == Bytes (intValue n), fromIntegral (V.length val) == natValue n ->
Mem.LLVMValArray eltStp (resolveMemVal eltType eltStp <$> val)
_ -> error $ "Unexpected storage type for packed vec."
-- | Report an unexpected value read from meory.
unexpectedMemVal :: Either String a
unexpectedMemVal = Left "Unexpected value read from memory."
-- | Translate from a memory value to a Crucible register value.
memValToCrucible ::
IsExpr (SymExpr sym) =>
MemRepr ty -> -- ^ Type of value to return
Mem.LLVMVal sym -> -- ^ Value to parse
Either String (RegValue sym (ToCrucibleType ty))
memValToCrucible memRep val =
case memRep of
-- Convert memory model value to pointer
M.BVMemRepr bytes _endian ->
do let bitw = natMultiply (knownNat @8) bytes
case val of
Mem.LLVMValInt base off
| Just Refl <- testEquality (bvWidth off) bitw ->
pure (Mem.LLVMPointer base off)
_ -> unexpectedMemVal
M.FloatMemRepr floatRep _endian ->
case val of
Mem.LLVMValFloat sz fltVal ->
case (floatRep, sz) of
(M.SingleFloatRepr, Mem.SingleSize) ->
pure fltVal
(M.DoubleFloatRepr, Mem.DoubleSize) ->
pure fltVal
(M.X86_80FloatRepr, Mem.X86_FP80Size) ->
pure fltVal
_ -> unexpectedMemVal
_ -> unexpectedMemVal
M.PackedVecMemRepr _expectedLen eltMemRepr -> do
case val of
Mem.LLVMValArray _ v -> do
traverse (memValToCrucible eltMemRepr) v
_ -> unexpectedMemVal
-- | Given a Boolean condition and two symbolic values associated with a Macaw type, return
-- a value denoting the first value if condition is true and second value otherwise.
muxMemReprValue ::
IsSymInterface sym =>
sym -> -- ^ Symbolic interface.
MemRepr ty -> -- ^ Description of memory layout of value
RegValue sym BoolType -> -- ^ Condition
RegValue sym (ToCrucibleType ty) -> -- ^ Value if condition is true
RegValue sym (ToCrucibleType ty) -> -- ^ Value if condition is false.
IO (RegValue sym (ToCrucibleType ty))
muxMemReprValue sym memRep cond x y =
case memRep of
M.BVMemRepr bytes _endian ->
case leqMulPos (knownNat @8) bytes of
LeqProof -> muxLLVMPtr sym cond x y
M.FloatMemRepr _floatRep _endian ->
baseTypeIte sym cond x y
M.PackedVecMemRepr _ eltMemRepr -> do
when (V.length x /= V.length y) $ do
throwIO $ userError $ "Expected vectors to have same length"
V.zipWithM (muxMemReprValue sym eltMemRepr cond) x y
-- | Use addr width to bring `HasPtrWidth` constraints in scope.
hasPtrClass :: M.AddrWidthRepr ptrW -> (Mem.HasPtrWidth ptrW => a) -> a
hasPtrClass ptrWidth v =
let ?ptrWidth = M.addrWidthNatRepr ptrWidth
in case ptrWidth of
M.Addr32 -> v
M.Addr64 -> v
doReadMem ::
IsSymInterface sym =>
CrucibleState s sym ext rtp blocks r ctx {- ^ Simulator state -} ->
GlobalVar Mem ->
GlobalMap sym ptrW ->
sym ->
MemImpl sym ->
M.AddrWidthRepr ptrW ->
MemRepr ty ->
RegEntry sym (LLVMPointerType ptrW) ->
IO ( RegValue sym (ToCrucibleType ty)
, CrucibleState s sym ext rtp blocks r ctx
)
doReadMem st mvar globs w (BVMemRepr bytes endian) ptr0 =
do mem <- getMem st mvar
checkEndian mem endian
LLVMPtr sym ptrW ->
IO (RegValue sym (ToCrucibleType ty))
doReadMem sym mem ptrWidth memRep ptr = hasPtrClass ptrWidth $
do -- Check pointer is valid.
-- Note. I think we should check that pointer has at least "bytes" bytes available?
ok <- isValidPtr sym mem ptrWidth ptr
check sym ok "doReadMem" $
"Reading through an invalid pointer: " ++ show (Mem.ppPtr ptr)
ty <- case memReprToStorageType (getEnd mem) memRep of
Left msg -> throwIO $ userError msg
Right tp -> pure tp
let sym = st^.stateSymInterface
ty = bitvectorType (toBytes (widthVal bytes))
bitw = natMultiply (knownNat @8) bytes
LeqProof <- return (leqMulPos (knownNat @8) bytes)
ptr <- tryGlobPtr sym mem globs (regValue ptr0)
let ?ptrWidth = M.addrWidthNatRepr w
ok <- isValidPtr sym mem w ptr
check sym ok "doReadMem"
$ "Reading through an invalid pointer: " ++ show (ppPtr ptr)
LeqProof <- pure $ addrWidthIsPos w
LeqProof <- pure $ addrWidthAtLeast16 w
let alignment = noAlignment -- default to byte alignment (FIXME)
val <- loadRaw sym mem ptr ty alignment
a <- case valToBits bitw val of
Just a -> return a
Nothing -> fail "[doReadMem] We read an unexpected value"
return (a,st)
-- Load a value from the memory model type system.
res <- Mem.loadRawWithCondition sym mem ptr ty alignment
-- Parse value returned by memory.
case res of
Left e -> do
addFailedAssertion sym (AssertFailureSimError e)
Right (memVal, isAlloc, isAlign, isValid) ->
case memValToCrucible memRep memVal of
Left err -> fail $ "[doReadMem] " ++ err
Right crucVal ->
do assert sym isAlloc (AssertFailureSimError "Read from unallocated memory")
assert sym isAlign (AssertFailureSimError "Read from unaligned memory")
assert sym isValid (AssertFailureSimError "Invalid memory load")
return crucVal
doCondReadMem ::
IsSymInterface sym =>
CrucibleState s sym ext rtp blocks r ctx {- ^ Simulator state -} ->
GlobalVar Mem {- ^ Memory model -} ->
GlobalMap sym ptrW {- ^ Translate machine addresses to memory model addresses -} ->
sym ->
MemImpl sym ->
M.AddrWidthRepr ptrW {- ^ Width of ptr -} ->
MemRepr ty {- ^ What/how we are reading -} ->
RegEntry sym BoolType {- ^ Condition -} ->
RegEntry sym (LLVMPointerType ptrW) {- ^ Pointer -} ->
RegEntry sym (ToCrucibleType ty) {- ^ Default answer -} ->
IO ( RegValue sym (ToCrucibleType ty)
, CrucibleState s sym ext rtp blocks r ctx
)
doCondReadMem st mvar globs w (BVMemRepr bytes endian) cond0 ptr0 def0 =
do let cond = regValue cond0
def = regValue def0
mem <- getMem st mvar
checkEndian mem endian
let sym = st^.stateSymInterface
ty = bitvectorType (toBytes (widthVal bytes))
bitw = natMultiply (knownNat @8) bytes
RegValue sym BoolType {- ^ Condition -} ->
LLVMPtr sym ptrW -> -- ^ Address to read
RegValue sym (ToCrucibleType ty) {- ^ Answer is condition is false -} ->
IO (RegValue sym (ToCrucibleType ty))
doCondReadMem sym mem ptrWidth memRep cond ptr def = hasPtrClass ptrWidth $
do -- Check pointer is valid.
-- Note. I think we should check that pointer has at least "bytes" bytes available?
ok <- isValidPtr sym mem ptrWidth ptr
check sym ok "doCondReadMem" $
"Conditional read through an invalid pointer: " ++ show (Mem.ppPtr ptr)
LeqProof <- return (leqMulPos (knownNat @8) bytes)
ty <- case memReprToStorageType (getEnd mem) memRep of
Left msg -> throwIO $ userError msg
Right tp -> pure tp
ptr <- tryGlobPtr sym mem globs (regValue ptr0)
ok <- isValidPtr sym mem w ptr
check sym ok "doCondReadMem"
$ "Conditional read through an invalid pointer: " ++
show (ppPtr ptr)
LeqProof <- pure $ addrWidthIsPos w
LeqProof <- pure $ addrWidthAtLeast16 w
let alignment = noAlignment -- default to byte alignment (FIXME)
val <- let ?ptrWidth = M.addrWidthNatRepr w
in loadRawWithCondition sym mem ptr ty alignment
val <- Mem.loadRawWithCondition sym mem ptr ty alignment
let useDefault msg =
do notC <- notPred sym cond
assert sym notC
(AssertFailureSimError ("[doCondReadMem] " ++ msg))
(AssertFailureSimError ("[doCondReadMem] " ++ msg))
return def
case val of
Left err -> useDefault err
Right (memVal, isAlloc, isAlign, isValid) ->
case memValToCrucible memRep memVal of
Left err -> useDefault err
Right crucVal ->
do do grd <- impliesPred sym cond isAlloc
assert sym grd (AssertFailureSimError (Mem.ptrMessage "Unallocated memory read" ptr ty))
do grd <- impliesPred sym cond isAlign
assert sym grd (AssertFailureSimError (Mem.ptrMessage "Unaligned memory read" ptr ty))
do grd <- impliesPred sym cond isValid
assert sym grd (AssertFailureSimError (Mem.ptrMessage "Invalid memory read" ptr ty))
muxMemReprValue sym memRep cond crucVal def
a <- case val of
Right (v, isAlloc, isAlign, isValid) | Just a <- valToBits bitw v ->
do let ?ptrWidth = M.addrWidthNatRepr w
do grd <- impliesPred sym cond isAlloc
assert sym grd (AssertFailureSimError (ptrMessage "Unallocated memory read" ptr ty))
do grd <- impliesPred sym cond isAlign
assert sym grd (AssertFailureSimError (ptrMessage "Unaligned memory read" ptr ty))
do grd <- impliesPred sym cond isValid
assert sym grd (AssertFailureSimError (ptrMessage "Invalid memory read" ptr ty))
muxLLVMPtr sym cond a def
Right _ -> useDefault "Unexpected value read from memory."
Left err -> useDefault err
return (a,st)
-- | Write a Macaw value to memory.
doWriteMem ::
IsSymInterface sym =>
CrucibleState s sym ext rtp blocks r ctx {- ^ Simulator state -} ->
GlobalVar Mem {- ^ Memory model -} ->
GlobalMap sym ptrW ->
M.AddrWidthRepr ptrW {- ^ Width of ptr -} ->
MemRepr ty {- ^ What/how we are writing -} ->
RegEntry sym (LLVMPointerType ptrW) {- ^ Pointer -} ->
RegEntry sym (ToCrucibleType ty) {- ^ Write this value -} ->
IO ( RegValue sym UnitType
, CrucibleState s sym ext rtp blocks r ctx
)
doWriteMem st mvar globs w (BVMemRepr bytes endian) ptr0 val =
do mem <- getMem st mvar
checkEndian mem endian
let sym = st^.stateSymInterface
ty = bitvectorType (toBytes (widthVal bytes))
LeqProof <- pure $ addrWidthIsPos w
LeqProof <- pure $ addrWidthAtLeast16 w
LeqProof <- return (leqMulPos (knownNat @8) bytes)
ptr <- tryGlobPtr sym mem globs (regValue ptr0)
ok <- isValidPtr sym mem w ptr
check sym ok "doWriteMem"
$ "Write to an invalid location: " ++ show (ppPtr ptr)
let ?ptrWidth = M.addrWidthNatRepr w
let v0 = regValue val
v = LLVMValInt (ptrBase v0) (asBits v0)
let alignment = noAlignment -- default to byte alignment (FIXME)
mem1 <- storeRaw sym mem ptr ty alignment v
return ((), setMem st mvar mem1)
--------------------------------------------------------------------------------
-- Utilities
infix 0 ~>
(~>) :: a -> b -> (a,b)
x ~> y = (x,y)
endCase :: Monad m => a -> m ([b],a)
endCase r = return ([],r)
endCaseCheck :: Monad m => a -> b -> c -> m ([(a,b)],c)
endCaseCheck a b c = return ([(a,b)],c)
-- | The offset part of a pointer.
asBits :: LLVMPtr sym w -> RegValue sym (BVType w)
asBits = snd . llvmPointerView
-- | The base part of a point.
ptrBase :: LLVMPtr sym w -> RegValue sym NatType
ptrBase = fst . llvmPointerView
-- | Is this value a bit-vector (i.e., not a pointer).
-- Note that the NULL pointer is actually also a bit-vector.
isBitVec :: IsSymInterface sym => sym -> LLVMPtr sym w -> IO (Pred sym)
isBitVec sym p = natEq sym (ptrBase p) =<< natLit sym 0
-- | Classify the arguments, and continue.
ptrOp ::
( (1 <= w) =>
sym ->
RegValue sym Mem ->
M.AddrWidthRepr w ->
Pred sym -> Pred sym -> Pred sym -> Pred sym ->
LLVMPtr sym w -> LLVMPtr sym w -> IO a
) ->
PtrOp sym w a
ptrOp k st mvar w x0 y0 =
do mem <- getMem st mvar
LeqProof <- return (addrWidthIsPos w)
let sym = st^.stateSymInterface
x = regValue x0
y = regValue y0
xBits <- isBitVec sym x
yBits <- isBitVec sym y
xPtr <- notPred sym xBits
yPtr <- notPred sym yBits
a <- k sym mem w xPtr xBits yPtr yBits x y
return (a,st)
-- | Get the current model of the memory.
getMem :: CrucibleState s sym ext rtp blocks r ctx ->
GlobalVar Mem ->
IO (RegValue sym Mem)
getMem st mvar =
case lookupGlobal mvar (st ^. stateTree . actFrame . gpGlobals) of
Just mem -> return mem
Nothing -> fail ("Global heap value not initialized: " ++ show mvar)
setMem :: CrucibleState s sym ext rtp blocks r ctx ->
GlobalVar Mem ->
MemImpl sym ->
CrucibleState s sym ext rtp blocks r ctx
setMem st mvar mem =
st & stateTree . actFrame . gpGlobals %~ insertGlobal mvar mem
-- | Define an operation by cases.
cases ::
(IsSymInterface sym) =>
sym {- ^ Simulator -} ->
String {- ^ Name of operation (for assertions) -} ->
(sym -> Pred sym -> a -> a -> IO a) {- Mux results -} ->
Maybe a {- ^ Default: use this if none of the cases matched -} ->
[(Pred sym, IO ([(Pred sym,String)], a))]
{- ^ Cases: (predicate when valid, result + additional checks) -} ->
IO a
cases sym name mux def opts =
case def of
Just _ -> combine =<< mapM doCase opts
Nothing ->
do ok <- oneOf (map fst opts)
check sym ok name ("Invalid arguments for " ++ show name)
combine =<< mapM doCase opts
where
oneOf xs =
case xs of
[] -> return (falsePred sym) -- shouldn't happen
[p] -> return p
p : ps -> orPred sym p =<< oneOf ps
combine [] = fail "[bug] Empty cases"
combine [(p,a)] = case def of
Just d -> mux sym p a d
Nothing -> return a
combine ((p,a) : more) = mux sym p a =<< combine more
doCase (p,m) =
do (checks,a) <- m
mapM_ (subCheck p) checks
return (p,a)
subCheck cp (p,msg) =
do valid <- impliesPred sym cp p
check sym valid name msg
check :: IsSymInterface sym => sym -> Pred sym -> String -> String -> IO ()
check sym valid name msg = assert sym valid
$ AssertFailureSimError
$ "[" ++ name ++ "] " ++ msg
valToBits :: (IsSymInterface sym, 1 <= w) =>
NatRepr w -> LLVMVal sym -> Maybe (LLVMPtr sym w)
valToBits w val =
case val of
LLVMValInt base off | Just Refl <- testEquality (bvWidth off) w ->
return (LLVMPointer base off)
_ -> Nothing
checkEndian :: MemImpl sym -> M.Endianness -> IO ()
checkEndian mem endian =
case (endian, memEndian mem) of
(M.BigEndian, BigEndian) -> return ()
(M.LittleEndian, LittleEndian) -> return ()
(need,have) -> fail $ unlines [ "[doReadMem] Endian mismatch:"
, " *** Model: " ++ show have
, " *** Read : " ++ show need ]
-- | A fresh boolean variable
mkUndefinedBool ::
(IsSymInterface sym) => sym -> String -> IO (RegValue sym BoolType)
mkUndefinedBool sym nm =
mkUndefined sym (nm ++ "bool_") BaseBoolRepr
-- | A fresh bit-vector variable
mkUndefinedBV ::
(IsSymInterface sym, 1 <= w) =>
sym -> String -> NatRepr w -> IO (RegValue sym (BVType w))
mkUndefinedBV sym nm w =
mkUndefined sym (nm ++ "bv" ++ show w ++ "_") (BaseBVRepr w)
mkUndefined ::
(IsSymInterface sym) =>
sym -> String -> BaseTypeRepr t -> IO (RegValue sym (BaseToType t))
mkUndefined sym unm ty =
do let name = "undefined_" ++ unm
nm <- mkName name
freshConstant sym nm ty
mkName :: String -> IO SolverSymbol
mkName x = case userSymbol x of
Right v -> return v
Left err ->
fail $ unlines
[ "[bug] " ++ show x ++ " is not a valid identifier?"
, "*** " ++ show err
]
{- | Every now and then we encounter memory opperations that
just read/write to some constant. Normally, we do not allow
such things as we want memory to be allocated first.
However we need to make an exception for globals.
So, if we ever try to manipulate memory at some address
which is statically known to be a constant, we consult
the global map to see if we know about a correpsonding
address. If so, we use that for the memory operation.
See the documentation of 'GlobalMap' for details about how that translation can
be handled.
-}
tryGlobPtr ::
IsSymInterface sym =>
sym ->
RegValue sym Mem ->
GlobalMap sym w ->
LLVMPtr sym w ->
IO (LLVMPtr sym w)
tryGlobPtr sym mem mapBVAddress val
| Just 0 <- asNat (ptrBase val) = do
maddr <- mapBVAddress sym mem (ptrBase val) (asBits val)
return (fromMaybe val maddr)
| otherwise = return val
isAlignMask :: (IsSymInterface sym) => LLVMPtr sym w -> Maybe Integer
isAlignMask v =
do 0 <- asNat (ptrBase v)
let off = asBits v
w = fromInteger (intValue (bvWidth off))
k <- asUnsignedBV off
let (zeros,ones) = break (testBit k) (take w [ 0 .. ])
guard (all (testBit k) ones)
return (fromIntegral (length zeros))
MemImpl sym -> -- ^ Heap prior to write
M.AddrWidthRepr ptrW -> -- ^ Width of ptr
MemRepr ty -> -- ^ What/how we are writing
LLVMPtr sym ptrW -> -- ^ Address to write to
RegValue sym (ToCrucibleType ty) -> -- ^ Value to write
IO (MemImpl sym)
doWriteMem sym mem ptrWidth memRep ptr val = hasPtrClass ptrWidth $
do ok <- isValidPtr sym mem ptrWidth ptr
check sym ok "doWriteMem" $
"Write to an invalid location: " ++ show (Mem.ppPtr ptr)
ty <- case memReprToStorageType (getEnd mem) memRep of
Left msg -> throwIO $ userError msg
Right tp -> pure tp
let alignment = noAlignment -- default to byte alignment (FIXME)
let memVal = resolveMemVal memRep ty val
Mem.storeRaw sym mem ptr ty alignment memVal

26
symbolic/src/Data/Macaw/Symbolic/PersistentState.hs
View File

@ -61,6 +61,14 @@ import qualified Lang.Crucible.LLVM.MemModel as MM
------------------------------------------------------------------------
-- Type mappings
-- | Convert Macaw float types into Crucible float types
type family ToCrucibleFloatInfo (fi :: M.FloatInfo) :: C.FloatInfo where
ToCrucibleFloatInfo M.HalfFloat = C.HalfFloat
ToCrucibleFloatInfo M.SingleFloat = C.SingleFloat
ToCrucibleFloatInfo M.DoubleFloat = C.DoubleFloat
ToCrucibleFloatInfo M.QuadFloat = C.QuadFloat
ToCrucibleFloatInfo M.X86_80Float = C.X86_80Float
type family ToCrucibleTypeList (l :: [M.Type]) :: Ctx C.CrucibleType where
ToCrucibleTypeList '[] = EmptyCtx
ToCrucibleTypeList (h ': l) = ToCrucibleTypeList l ::> ToCrucibleType h
@ -72,18 +80,11 @@ type family ToCrucibleTypeList (l :: [M.Type]) :: Ctx C.CrucibleType where
-- Crucible as 'MM.LLVMPointerType', which are special bitvectors that can also
-- be pointers in the LLVM memory model.
type family ToCrucibleType (tp :: M.Type) :: C.CrucibleType where
ToCrucibleType (M.BVType w) = MM.LLVMPointerType w
ToCrucibleType (M.FloatType fi) = C.FloatType (ToCrucibleFloatInfo fi)
ToCrucibleType ('M.TupleType l) = C.StructType (ToCrucibleTypeList l)
ToCrucibleType M.BoolType = C.BaseToType C.BaseBoolType
-- | Convert Macaw float types into Crucible float types
type family ToCrucibleFloatInfo (fi :: M.FloatInfo) :: C.FloatInfo where
ToCrucibleFloatInfo M.HalfFloat = C.HalfFloat
ToCrucibleFloatInfo M.SingleFloat = C.SingleFloat
ToCrucibleFloatInfo M.DoubleFloat = C.DoubleFloat
ToCrucibleFloatInfo M.QuadFloat = C.QuadFloat
ToCrucibleFloatInfo M.X86_80Float = C.X86_80Float
ToCrucibleType (M.BVType w) = MM.LLVMPointerType w
ToCrucibleType (M.FloatType fi) = C.FloatType (ToCrucibleFloatInfo fi)
ToCrucibleType ('M.TupleType l) = C.StructType (ToCrucibleTypeList l)
ToCrucibleType M.BoolType = C.BaseToType C.BaseBoolType
ToCrucibleType ('M.VecType n tp) = C.VectorType (ToCrucibleType tp)
-- | Convert Crucible float types into Macaw float types
type family FromCrucibleFloatInfo (fi :: C.FloatInfo) :: M.FloatInfo where
@ -125,6 +126,7 @@ typeToCrucible tp =
M.BVTypeRepr w -> MM.LLVMPointerRepr w
M.FloatTypeRepr fi -> C.FloatRepr $ floatInfoToCrucible fi
M.TupleTypeRepr a -> C.StructRepr (typeListToCrucible a)
M.VecTypeRepr _n e -> C.VectorRepr (typeToCrucible e)
-- | Convert Macaw floating point run-time representatives into their Crucible equivalents
floatInfoToCrucible

3
x86/src/Data/Macaw/X86.hs
View File

@ -398,7 +398,9 @@ transferAbsValue r f =
X86IRem{} -> TopV
X86Div{} -> TopV
X86Rem{} -> TopV
SSE_UnaryOp{} -> TopV
SSE_VectorOp{} -> TopV
SSE_Sqrt{} -> TopV
SSE_CMPSX{} -> TopV
SSE_UCOMIS{} -> TopV
SSE_CVTSD2SS{} -> TopV
@ -419,7 +421,6 @@ transferAbsValue r f =
VExtractF128 {} -> TopV
VInsert {} -> TopV
-- | Disassemble block, returning either an error, or a list of blocks
-- and ending PC.
initRegsFromAbsState :: forall ids

188
x86/src/Data/Macaw/X86/ArchTypes.hs
View File

@ -15,7 +15,6 @@ module Data.Macaw.X86.ArchTypes
( -- * Architecture
X86_64
, X86PrimFn(..)
, X87_FloatType(..)
, SSE_FloatType(..)
, SSE_Cmp(..)
, lookupSSECmp
@ -31,6 +30,7 @@ module Data.Macaw.X86.ArchTypes
, X86TermStmt(..)
, rewriteX86TermStmt
, X86PrimLoc(..)
, SIMDByteCount(..)
, SIMDWidth(..)
, RepValSize(..)
, SomeRepValSize(..)
@ -60,7 +60,20 @@ import Data.Macaw.X86.X87ControlReg
-- SIMDWidth
-- | Defines a width of a register associated with SIMD operations
-- (e.g., MMX, XMM, AVX)
-- (e.g., MMX, XMM, YMM)
data SIMDByteCount w
= (w ~ 8) => SIMDByteCount_MMX
| (w ~ 16) => SIMDByteCount_XMM
| (w ~ 32) => SIMDByteCount_YMM
-- | Number of bytes in @SIMDByteCount@.
simdByteCountNatRepr :: SIMDByteCount w -> NatRepr w
simdByteCountNatRepr SIMDByteCount_MMX = n8
simdByteCountNatRepr SIMDByteCount_XMM = n16
simdByteCountNatRepr SIMDByteCount_YMM = n32
-- | Defines a width of a register associated with SIMD operations
-- (e.g., MMX, XMM, YMM)
data SIMDWidth w
= (w ~ 64) => SIMD_64
| (w ~ 128) => SIMD_128
@ -205,7 +218,6 @@ data SSE_Op
| SSE_Div
| SSE_Min
| SSE_Max
| SSE_Sqrt
-- | Return the name of the mnemonic associated with the SSE op.
sseOpName :: SSE_Op -> String
@ -217,34 +229,20 @@ sseOpName f =
SSE_Div -> "div"
SSE_Min -> "min"
SSE_Max -> "max"
SSE_Sqrt -> "sqrt"
-- | A single or double value for floating-point restricted to this types.
data SSE_FloatType tp where
SSE_Single :: SSE_FloatType (FloatBVType SingleFloat)
SSE_Double :: SSE_FloatType (FloatBVType DoubleFloat)
SSE_Single :: SSE_FloatType SingleFloat
SSE_Double :: SSE_FloatType DoubleFloat
instance Show (SSE_FloatType tp) where
show SSE_Single = "single"
show SSE_Double = "double"
instance HasRepr SSE_FloatType TypeRepr where
instance HasRepr SSE_FloatType FloatInfoRepr where
typeRepr SSE_Single = knownRepr
typeRepr SSE_Double = knownRepr
------------------------------------------------------------------------
-- X87 declarations
data X87_FloatType tp where
X87_Single :: X87_FloatType (FloatBVType SingleFloat)
X87_Double :: X87_FloatType (FloatBVType DoubleFloat)
X87_ExtDouble :: X87_FloatType (FloatBVType X86_80Float)
instance Show (X87_FloatType tp) where
show X87_Single = "single"
show X87_Double = "double"
show X87_ExtDouble = "extdouble"
------------------------------------------------------------------------
data AVXOp1 = VShiftL Word8 -- ^ Shift left by this many bytes
@ -369,12 +367,15 @@ data X86PrimFn f tp where
-- | @PShufb w x s@ returns a value @res@ generated from the bytes of @x@
-- based on indices defined in the corresponding bytes of @s@.
--
-- Let @n@ be the number of bytes in the width @w@, and let @l = log2(n)@.
-- Let @w@ be the number of bytes, and let @l = log2(n)@.
-- Given a byte index @i@, the value of byte @res[i]@, is defined by
-- @res[i] = 0 if msb(s[i]) == 1@
-- @res[i] = x[j] where j = s[i](0..l)
-- where @msb(y)@ returns the most-significant bit in byte @y@.
PShufb :: (1 <= w) => !(SIMDWidth w) -> !(f (BVType w)) -> !(f (BVType w)) -> X86PrimFn f (BVType w)
PShufb :: !(SIMDByteCount w)
-> !(f (VecType w (BVType 8)))
-> !(f (VecType w (BVType 8)))
-> X86PrimFn f (VecType w (BVType 8))
-- | Compares two memory regions and return the number of bytes that were the same.
--
@ -439,17 +440,32 @@ data X86PrimFn f tp where
-> !(f (BVType w))
-> X86PrimFn f (BVType w)
-- | This applies the operation pairwise to floating point values.
--
-- This function implicitly depends on the MXCSR register and may
-- signal exceptions as noted in the documentation on SSE.
SSE_UnaryOp :: !SSE_Op
-> !(SSE_FloatType tp)
-> !(f (FloatType tp))
-> !(f (FloatType tp))
-> X86PrimFn f (FloatType tp)
-- | This applies the operation pairwise to two vectors of floating point values.
--
-- This function implicitly depends on the MXCSR register and may
-- signal exceptions as noted in the documentation on SSE.
SSE_VectorOp :: (1 <= n, 1 <= w)
SSE_VectorOp :: 1 <= n
=> !SSE_Op
-> !(NatRepr n)
-> !(SSE_FloatType (BVType w))
-> !(f (BVType (n*w)))
-> !(f (BVType (n*w)))
-> X86PrimFn f (BVType (n*w))
-> !(SSE_FloatType tp)
-> !(f (VecType n (FloatType tp)))
-> !(f (VecType n (FloatType tp)))
-> X86PrimFn f (VecType n (FloatType tp))
-- | This computes the sqrt of the floating point value.
SSE_Sqrt :: !(SSE_FloatType tp)
-> !(f (FloatType tp))
-> X86PrimFn f (FloatType tp)
-- | This performs a comparison between the two instructions (as
-- needed by the CMPSD and CMPSS instructions.
@ -459,9 +475,9 @@ data X86PrimFn f tp where
-- appropriate bits are set on the MXCSR register.
SSE_CMPSX :: !SSE_Cmp
-> !(SSE_FloatType tp)
-> !(f tp)
-> !(f tp)
-> X86PrimFn f tp
-> !(f (FloatType tp))
-> !(f (FloatType tp))
-> X86PrimFn f BoolType
-- | This performs a comparison of two floating point values and returns three flags:
--
@ -478,8 +494,8 @@ data X86PrimFn f tp where
-- This function implicitly depends on the MXCSR register and may signal exceptions based
-- on the configuration of that register.
SSE_UCOMIS :: !(SSE_FloatType tp)
-> !(f tp)
-> !(f tp)
-> !(f (FloatType tp))
-> !(f (FloatType tp))
-> X86PrimFn f (TupleType [BoolType, BoolType, BoolType])
-- | This converts a single to a double precision number.
@ -487,14 +503,16 @@ data X86PrimFn f tp where
-- This function implicitly depends on the MXCSR register and may
-- signal a exception based on the configuration of that
-- register.
SSE_CVTSS2SD :: !(f (BVType 32)) -> X86PrimFn f (BVType 64)
SSE_CVTSS2SD :: !(f (FloatType SingleFloat))
-> X86PrimFn f (FloatType DoubleFloat)
-- | This converts a double to a single precision number.
--
-- This function implicitly depends on the MXCSR register and may
-- signal a exception based on the configuration of that
-- register.
SSE_CVTSD2SS :: !(f (BVType 64)) -> X86PrimFn f (BVType 32)
SSE_CVTSD2SS :: !(f (FloatType DoubleFloat))
-> X86PrimFn f (FloatType SingleFloat)
-- | This converts a floating point value to a bitvector of the
-- given width (should be 32 or 64)
@ -502,11 +520,11 @@ data X86PrimFn f tp where
-- This function implicitly depends on the MXCSR register and may
-- signal exceptions based on the configuration of that register.
SSE_CVTTSX2SI
:: (1 <= w)
=> !(NatRepr w)
:: (1 <= n)
=> !(NatRepr n)
-> !(SSE_FloatType tp)
-> !(f tp)
-> X86PrimFn f (BVType w)
-> !(f (FloatType tp))
-> X86PrimFn f (BVType n)
-- | This converts a signed integer to a floating point value of
-- the given type (the input width should be 32 or 64)
@ -518,13 +536,13 @@ data X86PrimFn f tp where
=> !(SSE_FloatType tp)
-> !(NatRepr w)
-> !(f (BVType w))
-> X86PrimFn f tp
-> X86PrimFn f (FloatType tp)
-- | Extends a single or double to 80-bit precision.
-- Guaranteed to not throw exception or have side effects.
X87_Extend :: !(SSE_FloatType tp)
-> !(f tp)
-> X86PrimFn f (FloatBVType X86_80Float)
-> !(f (FloatType tp))
-> X86PrimFn f (FloatType X86_80Float)
-- | This performs an 80-bit floating point add.
--
@ -540,9 +558,9 @@ data X86PrimFn f tp where
-- * @#U@ Result is too small for destination format.
-- * @#O@ Result is too large for destination format.
-- * @#P@ Value cannot be represented exactly in destination format.
X87_FAdd :: !(f (FloatBVType X86_80Float))
-> !(f (FloatBVType X86_80Float))
-> X86PrimFn f (TupleType [FloatBVType X86_80Float, BoolType])
X87_FAdd :: !(f (FloatType X86_80Float))
-> !(f (FloatType X86_80Float))
-> X86PrimFn f (TupleType [FloatType X86_80Float, BoolType])
-- | This performs an 80-bit floating point subtraction.
--
@ -558,9 +576,9 @@ data X86PrimFn f tp where
-- * @#U@ Result is too small for destination format.
-- * @#O@ Result is too large for destination format.
-- * @#P@ Value cannot be represented exactly in destination format.
X87_FSub :: !(f (FloatBVType X86_80Float))
-> !(f (FloatBVType X86_80Float))
-> X86PrimFn f (TupleType [FloatBVType X86_80Float, BoolType])
X87_FSub :: !(f (FloatType X86_80Float))
-> !(f (FloatType X86_80Float))
-> X86PrimFn f (TupleType [FloatType X86_80Float, BoolType])
-- | This performs an 80-bit floating point multiply.
--
@ -576,9 +594,9 @@ data X86PrimFn f tp where
-- * @#U@ Result is too small for destination format.
-- * @#O@ Result is too large for destination format.
-- * @#P@ Value cannot be represented exactly in destination format.
X87_FMul :: !(f (FloatBVType X86_80Float))
-> !(f (FloatBVType X86_80Float))
-> X86PrimFn f (TupleType [FloatBVType X86_80Float, BoolType])
X87_FMul :: !(f (FloatType X86_80Float))
-> !(f (FloatType X86_80Float))
-> X86PrimFn f (TupleType [FloatType X86_80Float, BoolType])
-- | This rounds a floating number to single or double precision.
--
@ -594,8 +612,8 @@ data X86PrimFn f tp where
-- In the #P case, the C1 register will be set 1 if rounding up,
-- and 0 otherwise.
X87_FST :: !(SSE_FloatType tp)
-> !(f (FloatBVType X86_80Float))
-> X86PrimFn f tp
-> !(f (FloatType X86_80Float))
-> X86PrimFn f (FloatType tp)
-- | Unary operation on a vector. Should have no side effects.
--
@ -604,11 +622,11 @@ data X86PrimFn f tp where
-- * @w@ is the width of the input/result vector
-- * @op@ is the operation to perform
-- * @tgt@ is the target vector of the operation
VOp1 :: (1 <= n) =>
!(NatRepr n) ->
!AVXOp1 ->
!(f (BVType n)) ->
X86PrimFn f (BVType n)
VOp1 :: (1 <= n)
=> !(NatRepr n)
-> !AVXOp1
-> !(f (BVType n))
-> X86PrimFn f (BVType n)
-- | Binary operation on two vectors. Should not have side effects.
--
@ -618,12 +636,12 @@ data X86PrimFn f tp where
-- * @op@ is the binary operation to perform on the vectors
-- * @vec1@ is the first vector
-- * @vec2@ is the second vector
VOp2 :: (1 <= n) =>
!(NatRepr n) ->
!AVXOp2 ->
!(f (BVType n)) ->
!(f (BVType n)) ->
X86PrimFn f (BVType n)
VOp2 :: (1 <= n)
=> !(NatRepr n)
-> !AVXOp2
-> !(f (BVType n))
-> !(f (BVType n))
-> X86PrimFn f (BVType n)
-- | Update an element of a vector.
--
@ -669,21 +687,20 @@ data X86PrimFn f tp where
-- * @op@ is the binary operation to perform on the vectors
-- * @vec1@ is the first vector
-- * @vec2@ is the second vector
Pointwise2 :: (1 <= elSize, 1 <= elNum) =>
!(NatRepr elNum)
Pointwise2 :: (1 <= elSize, 1 <= elNum)
=> !(NatRepr elNum)
-> !(NatRepr elSize)
-> !AVXPointWiseOp2
-> !(f (BVType (elNum * elSize)))
-> !(f (BVType (elNum * elSize)))
-> X86PrimFn f (BVType (elNum * elSize))
{- | Extract 128 bits from a 256 bit value, as described by the
control mask -}
VExtractF128 ::
!(f (BVType 256)) ->
!Word8 ->
X86PrimFn f (BVType 128)
-- | Extract 128 bits from a 256 bit value, as described by the
-- control mask
VExtractF128
:: !(f (BVType 256))
-> !Word8
-> X86PrimFn f (BVType 128)
instance HasRepr (X86PrimFn f) TypeRepr where
@ -697,7 +714,7 @@ instance HasRepr (X86PrimFn f) TypeRepr where
CMPXCHG8B{} -> knownRepr
RDTSC{} -> knownRepr
XGetBV{} -> knownRepr
PShufb w _ _ -> BVTypeRepr (typeRepr w)
PShufb w _ _ -> VecTypeRepr (simdByteCountNatRepr w) knownRepr
MemCmp{} -> knownRepr
RepnzScas{} -> knownRepr
MMXExtend{} -> knownRepr
@ -705,18 +722,20 @@ instance HasRepr (X86PrimFn f) TypeRepr where
X86IRem w _ _ -> typeRepr (repValSizeMemRepr w)
X86Div w _ _ -> typeRepr (repValSizeMemRepr w)
X86Rem w _ _ -> typeRepr (repValSizeMemRepr w)
SSE_VectorOp _ w tp _ _ -> packedType w tp
SSE_CMPSX _ tp _ _ -> typeRepr tp
SSE_UnaryOp _ tp _ _ -> FloatTypeRepr (typeRepr tp)
SSE_VectorOp _ w tp _ _ -> VecTypeRepr w (FloatTypeRepr (typeRepr tp))
SSE_Sqrt tp _ -> FloatTypeRepr (typeRepr tp)
SSE_CMPSX{} -> knownRepr
SSE_UCOMIS _ _ _ -> knownRepr
SSE_CVTSS2SD{} -> knownRepr
SSE_CVTSD2SS{} -> knownRepr
SSE_CVTSI2SX tp _ _ -> typeRepr tp
SSE_CVTSI2SX tp _ _ -> FloatTypeRepr (typeRepr tp)
SSE_CVTTSX2SI w _ _ -> BVTypeRepr w
X87_Extend{} -> knownRepr
X87_FAdd{} -> knownRepr
X87_FSub{} -> knownRepr
X87_FMul{} -> knownRepr
X87_FST tp _ -> typeRepr tp
X87_FST tp _ -> FloatTypeRepr (typeRepr tp)
PointwiseShiftL n w _ _ _ -> packedAVX n w
VInsert n w _ _ _ -> packedAVX n w
VOp1 w _ _ -> BVTypeRepr w
@ -730,11 +749,6 @@ packedAVX n w =
case leqMulPos n w of
LeqProof -> BVTypeRepr (natMultiply n w)
packedType :: (1 <= n, 1 <= w) => NatRepr n -> SSE_FloatType (BVType w) -> TypeRepr (BVType (n*w))
packedType w tp =
case leqMulPos w (typeWidth tp) of
LeqProof -> BVTypeRepr (natMultiply w (typeWidth tp))
instance FunctorFC X86PrimFn where
fmapFC = fmapFCDefault
@ -762,7 +776,9 @@ instance TraversableFC X86PrimFn where
X86IRem w n d -> X86IRem w <$> go n <*> go d
X86Div w n d -> X86Div w <$> go n <*> go d
X86Rem w n d -> X86Rem w <$> go n <*> go d
SSE_UnaryOp op tp x y -> SSE_UnaryOp op tp <$> go x <*> go y
SSE_VectorOp op n tp x y -> SSE_VectorOp op n tp <$> go x <*> go y
SSE_Sqrt ftp x -> SSE_Sqrt ftp <$> go x
SSE_CMPSX c tp x y -> SSE_CMPSX c tp <$> go x <*> go y
SSE_UCOMIS tp x y -> SSE_UCOMIS tp <$> go x <*> go y
SSE_CVTSS2SD x -> SSE_CVTSS2SD <$> go x
@ -806,14 +822,18 @@ instance IsArchFn X86PrimFn where
X86IRem w n d -> sexprA "irem" [ ppShow $ typeWidth $ repValSizeMemRepr w, pp n, pp d ]
X86Div w n d -> sexprA "div" [ ppShow $ typeWidth $ repValSizeMemRepr w, pp n, pp d ]
X86Rem w n d -> sexprA "rem" [ ppShow $ typeWidth $ repValSizeMemRepr w, pp n, pp d ]
SSE_UnaryOp op tp x y ->
sexprA ("sse_" ++ sseOpName op ++ "1") [ ppShow tp, pp x, pp y ]
SSE_VectorOp op n tp x y ->
sexprA ("sse_" ++ sseOpName op) [ ppShow n, ppShow tp, pp x, pp y ]
SSE_Sqrt ftp x ->
sexprA "sse_sqrt" [ ppShow ftp, pp x ]
SSE_CMPSX c tp x y -> sexprA "sse_cmpsx" [ ppShow c, ppShow tp, pp x, pp y ]
SSE_UCOMIS _ x y -> sexprA "ucomis" [ pp x, pp y ]
SSE_CVTSS2SD x -> sexprA "cvtss2sd" [ pp x ]
SSE_CVTSD2SS x -> sexprA "cvtsd2ss" [ pp x ]
SSE_CVTSI2SX tp w x -> sexprA "cvtsi2sx" [ ppShow tp, ppShow w, pp x ]
SSE_CVTTSX2SI w tp x -> sexprA "cvttsx2si" [ ppShow w, ppShow tp, pp x ]
SSE_CVTTSX2SI n tp x -> sexprA "cvttsx2si" [ ppShow n, ppShow tp, pp x ]
X87_Extend tp x -> sexprA "x87_extend" [ ppShow tp, pp x ]
X87_FAdd x y -> sexprA "x87_add" [ pp x, pp y ]
X87_FSub x y -> sexprA "x87_sub" [ pp x, pp y ]
@ -857,7 +877,9 @@ x86PrimFnHasSideEffects f =
X86Rem{} -> True -- /\ ..
-- Each of these may throw exceptions based on floating point config flags.
SSE_UnaryOp{} -> True
SSE_VectorOp{} -> True
SSE_Sqrt{} -> True
SSE_CMPSX{} -> True
SSE_UCOMIS{} -> True
SSE_CVTSS2SD{} -> True

1
x86/src/Data/Macaw/X86/Generator.hs
View File

@ -20,6 +20,7 @@ module Data.Macaw.X86.Generator
X86Generator(..)
, runX86Generator
, X86GCont
, addAssignment
, addStmt
, addTermStmt
, addArchStmt

6
x86/src/Data/Macaw/X86/Getters.hs
View File

@ -44,6 +44,7 @@ module Data.Macaw.X86.Getters
, wordMemRepr
, dwordMemRepr
, qwordMemRepr
, x87MemRepr
, xmmMemRepr
, ymmMemRepr
) where
@ -221,7 +222,10 @@ readBVAddress ar repr = get . (`MemoryAddr` repr) =<< getBVAddress ar
data SomeBV v where
SomeBV :: SupportedBVWidth n => v (BVType n) -> SomeBV v
-- | Maps float info repr to associated MemRepr.
floatMemRepr :: FloatInfoRepr fi -> MemRepr (FloatBVType fi)
floatMemRepr fi | LeqProof <- floatInfoBytesIsPos fi =
BVMemRepr (floatInfoBytes fi) LittleEndian
-- | Extract the location of a bitvector value.
getSomeBVLocation :: F.Value -> X86Generator st ids (SomeBV (Location (Addr ids)))

32
x86/src/Data/Macaw/X86/InstructionDef.hs
View File

@ -20,9 +20,6 @@ module Data.Macaw.X86.InstructionDef
, defNullaryPrefix
-- * Unary instruction helpers
, defUnary
, defUnaryLoc
, defUnaryKnown
, defUnaryV
-- * Binary instruction helpers
, defBinary
, defBinaryLV
@ -95,35 +92,6 @@ defUnary mnem f = defVariadic mnem $ \pfx vs ->
[v] -> f pfx v
_ -> fail $ "defUnary: " ++ mnem ++ " expecting 1 arguments, got " ++ show (length vs)
-- | Defines an instruction that expects a single bitvec location as an argument.
defUnaryLoc :: String
-> (forall st ids n
. SupportedBVWidth n
=> Location (Addr ids) (BVType n)
-> X86Generator st ids ())
-> InstructionDef
defUnaryLoc s f = defUnary s $ \_ val -> do
SomeBV v <- getSomeBVLocation val
f v
-- | Defines an instruction that expects a bitvector location with a known fixed width.
defUnaryKnown :: KnownNat n
=> String
-> (forall st ids . Location (Addr ids) (BVType n) -> X86Generator st ids ())
-> InstructionDef
defUnaryKnown s f = defUnary s $ \_ loc -> f =<< getBVLocation loc knownNat
-- | Defines an instruction that expects a single bitvec value as an argument.
defUnaryV :: String
-> ( forall st ids n
. SupportedBVWidth n
=> Expr ids (BVType n)
-> X86Generator st ids ())
-> InstructionDef
defUnaryV s f = defUnary s $ \_ val -> do
SomeBV v <- getSomeBVValue val
f v
-- | Define an instruction that expects two arguments.
defBinary :: String
-> (forall st ids

13
x86/src/Data/Macaw/X86/Monad.hs
View File

@ -32,7 +32,6 @@ module Data.Macaw.X86.Monad
, repValSizeMemRepr
, Data.Macaw.Types.FloatInfoRepr(..)
, Data.Macaw.Types.floatInfoBits
, floatMemRepr
-- * RegisterView
, RegisterView
, RegisterViewType(..)
@ -71,7 +70,6 @@ module Data.Macaw.X86.Monad
, c2_loc
, c3_loc
, mkFPAddr
, packWord
, unpackWord
-- ** Registers
@ -124,6 +122,7 @@ module Data.Macaw.X86.Monad
, bvRor
, bvTrunc'
, bvTrunc
-- , bitcast
, msb
, least_byte
, least_nibble
@ -176,7 +175,6 @@ import Control.Lens hiding ((.=))
import Control.Monad
import qualified Data.Bits as Bits
import Data.Macaw.CFG
import Data.Macaw.Memory (Endianness(..))
import Data.Macaw.Types
import Data.Maybe
import Data.Parameterized.Classes
@ -743,15 +741,6 @@ c1_loc = fullRegister R.X87_C1
c2_loc = fullRegister R.X87_C2
c3_loc = fullRegister R.X87_C3
-- | Maps float info repr to associated MemRepr.
floatMemRepr :: FloatInfoRepr fi -> MemRepr (FloatBVType fi)
floatMemRepr fi | LeqProof <- floatInfoBytesIsPos fi =
BVMemRepr (floatInfoBytes fi) LittleEndian
-- | Tuen an address into a location of size @n
mkFPAddr :: FloatInfoRepr fi -> addr -> Location addr (FloatBVType fi)
mkFPAddr fi addr = MemoryAddr addr (floatMemRepr fi)
-- | Return MMX register corresponding to x87 register.
--
-- An MMX register is the low 64-bits of an x87 register. These

388
x86/src/Data/Macaw/X86/Semantics.hs
View File

@ -11,6 +11,7 @@ This module provides definitions for x86 instructions.
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE NondecreasingIndentation #-}
@ -36,9 +37,10 @@ import qualified Flexdis86 as F
import Data.Macaw.CFG ( MemRepr(..)
, memReprBytes
, App(..)
, Value(BoolValue)
, AssignRhs(CondReadMem)
, Value(BoolValue, AssignedValue)
, AssignRhs(CondReadMem, ReadMem)
, mkLit
, WidthEqProof(..)
)
import Data.Macaw.Memory (Endianness (LittleEndian))
import Data.Macaw.Types
@ -56,7 +58,45 @@ import qualified Data.Macaw.X86.Semantics.AVX as AVX
type Addr s = Expr s (BVType 64)
type BVExpr ids w = Expr ids (BVType w)
-- * Preliminaries
------------------------------------------------------------------------
-- Casting operations
bitcast :: WidthEqProof i o -> Expr ids i -> Expr ids o
bitcast p x = app (Bitcast x p)
toSingle :: WidthEqProof (BVType 32) (FloatType SingleFloat)
toSingle = ToFloat SingleFloatRepr
fromSingle :: WidthEqProof (FloatType SingleFloat) (BVType 32)
fromSingle = FromFloat SingleFloatRepr
toDouble :: WidthEqProof (BVType 64) (FloatType DoubleFloat)
toDouble = ToFloat DoubleFloatRepr
fromDouble :: WidthEqProof (FloatType DoubleFloat) (BVType 64)
fromDouble = FromFloat DoubleFloatRepr
toX87Float :: WidthEqProof (BVType 80) (FloatType X86_80Float)
toX87Float = ToFloat X86_80FloatRepr
fromX87Float :: WidthEqProof (FloatType X86_80Float) (BVType 80)
fromX87Float = FromFloat X86_80FloatRepr
toXMMBytes :: WidthEqProof (BVType 128) (VecType 16 (BVType 8))
toXMMBytes = UnpackBits n16 n8
fromXMMBytes :: WidthEqProof (VecType 16 (BVType 8)) (BVType 128)
fromXMMBytes = PackBits n16 n8
castToXMMSingleVec :: Expr ids (BVType 128) -> Expr ids (VecType 4 (FloatType SingleFloat))
castToXMMSingleVec = bitcast (VecEqCongruence n4 toSingle) . bitcast (UnpackBits n4 n32)
castFromXMMSingleVec :: Expr ids (VecType 4 (FloatType SingleFloat)) -> Expr ids (BVType 128)
castFromXMMSingleVec = bitcast (PackBits n4 n32) . bitcast (VecEqCongruence n4 fromSingle)
------------------------------------------------------------------------
-- Preliminaries
-- The representation for a address
addrRepr :: MemRepr (BVType 64)
@ -148,6 +188,25 @@ getRM32_RM64 v =
F.Mem64 addr -> Right <$> getBV64Addr addr
_ -> fail "Unexpected operand"
-- | The the low bits in a register.
setLowBits :: forall st_s ids l w
. (1 <= l, l <= w, KnownNat l, KnownNat w)
=> X86Reg (BVType w)
-> Expr ids (BVType l)
-> X86Generator st_s ids ()
setLowBits r e = do
let w :: NatRepr w
w = knownNat
let l :: NatRepr l
l = knownNat
-- Get initial value
v0 <- getReg r
-- Get old bits
LeqProof <- pure $ leqTrans (LeqProof @1 @l) (LeqProof @l @w)
let prevBits = v0 .&. bvLit w (Bits.complement (maxUnsigned l))
-- Or prevBits with new value
v1 <- eval $ prevBits .|. uext w e
setReg r v1
-- | Location that get the low 32 bits of a XMM register,
-- and preserves the high 64 bits on writes.
@ -161,7 +220,7 @@ xmm_low64 r = subRegister n0 n64 (xmmOwner r)
-- | Location that get the low 64 bits of a XMM register,
-- and preserves the high 64 bits on writes.
xmm_low :: F.XMMReg -> SSE_FloatType tp -> Location addr tp
xmm_low :: F.XMMReg -> SSE_FloatType tp -> Location addr (FloatBVType tp)
xmm_low r SSE_Single = xmm_low32 r
xmm_low r SSE_Double = xmm_low64 r
@ -170,47 +229,57 @@ xmm_low r SSE_Double = xmm_low64 r
xmm_high64 :: F.XMMReg -> Location addr (BVType 64)
xmm_high64 r = subRegister n64 n64 (xmmOwner r)
-- | This gets the register of a xmm field.
getXMM :: Monad m => F.Value -> m F.XMMReg
getXMM (F.XMMReg r) = pure r
getXMM _ = fail "Unexpected argument"
singleMemRepr :: MemRepr (FloatType SingleFloat)
singleMemRepr = FloatMemRepr SingleFloatRepr LittleEndian
-- | This gets the value of a xmm/m32 field.
--
-- If it is an XMM value, it gets the low 32bit register.
-- If it is a memory address is gets the 32bits there.
-- Otherwise it fails.
getXMM_mr_low32 :: F.Value -> X86Generator st ids (Location (Addr ids) (BVType 32))
getXMM_mr_low32 (F.XMMReg r) = pure (xmm_low32 r)
getXMM_mr_low32 (F.Mem128 src_addr) = getBV32Addr src_addr
getXMM_mr_low32 _ = fail "Unexpected argument"
doubleMemRepr :: MemRepr (FloatType DoubleFloat)
doubleMemRepr = FloatMemRepr DoubleFloatRepr LittleEndian
xmmSingleMemRepr :: MemRepr (VecType 4 (FloatType SingleFloat))
xmmSingleMemRepr = PackedVecMemRepr n4 singleMemRepr
readMem :: F.AddrRef -> MemRepr tp -> X86Generator st ids (Value X86_64 ids tp)
readMem addrRef repr = do
addr <- eval =<< getBVAddress addrRef
AssignedValue <$> addAssignment (ReadMem addr repr)
getXMMreg_float_low :: F.XMMReg -> SSE_FloatType tp -> X86Generator st ids (Value X86_64 ids (FloatType tp))
getXMMreg_float_low r SSE_Single =
eval . bitcast toSingle . bvTrunc' n32 =<< getReg (xmmOwner r)
getXMMreg_float_low r SSE_Double =
eval . bitcast toDouble . bvTrunc' n64 =<< getReg (xmmOwner r)
-- | This gets the value of a xmm/m128 field as 4 floats
getXMMreg_sv :: F.XMMReg -> X86Generator st ids (Value X86_64 ids (VecType 4 (FloatType SingleFloat)))
getXMMreg_sv r = eval . castToXMMSingleVec . bvTrunc' n128 =<< getReg (xmmOwner r)
-- | This gets the value of a xmm/m128 field as 4 floats
getXMM_sv :: F.Value -> X86Generator st ids (Value X86_64 ids (VecType 4 (FloatType SingleFloat)))
getXMM_sv (F.XMMReg r) = getXMMreg_sv r
getXMM_sv (F.Mem128 addrRef) = readMem addrRef xmmSingleMemRepr
getXMM_sv _ = fail "Unexpected argument"
-- | This gets the value of a xmm/m128 field as 4 floats
setXMMreg_sv :: F.XMMReg -> Expr ids (VecType 4 (FloatType SingleFloat)) -> X86Generator st ids ()
setXMMreg_sv r e = setLowBits (xmmOwner r) (castFromXMMSingleVec e)
-- | This gets the value of a xmm/m64 field.
--
-- If it is an XMM value, it gets the low 64bit register.
-- If it is a memory address is gets the 64bits there.
-- Otherwise it fails.
getXMM_mr_low64 :: F.Value -> X86Generator st ids (Location (Addr ids) (BVType 64))
getXMM_mr_low64 (F.XMMReg r) = pure (xmm_low64 r)
getXMM_mr_low64 (F.Mem128 src_addr) = getBV64Addr src_addr
getXMM_mr_low64 _ = fail "Unexpected argument"
getXMM_float_low :: F.Value -> SSE_FloatType tp -> X86Generator st ids (Value X86_64 ids (FloatType tp))
getXMM_float_low (F.XMMReg r) tp = getXMMreg_float_low r tp
getXMM_float_low (F.Mem128 addrRef) SSE_Single = readMem addrRef singleMemRepr
getXMM_float_low (F.Mem128 addrRef) SSE_Double = readMem addrRef doubleMemRepr
getXMM_float_low _ _ = fail "Unexpected argument"
-- | This gets the value of a xmm/m64 field.
--
-- If it is an XMM value, it gets the low 64bit register.
-- If it is a memory address is gets the 64bits there.
-- Otherwise it fails.
getXMM_mr_low :: F.Value -> SSE_FloatType tp -> X86Generator st ids (Location (Addr ids) tp)
getXMM_mr_low (F.XMMReg r) tp = pure (xmm_low r tp)
getXMM_mr_low (F.Mem128 src_addr) SSE_Single = getBV32Addr src_addr
getXMM_mr_low (F.Mem128 src_addr) SSE_Double = getBV64Addr src_addr
getXMM_mr_low _ _ = fail "Unexpected argument"
-- | This gets the value of a xmm/m128 field.
getXMM_mr :: F.Value -> X86Generator st ids (Location (Addr ids) (BVType 128))
getXMM_mr v@(F.XMMReg {}) = getBVLocation v n128
getXMM_mr v@(F.Mem128 {}) = getBVLocation v n128
getXMM_mr _ = fail "Unexpected argument"
-- | The the least significant float or double in an XMM register
setXMMreg_float_low :: F.XMMReg -> SSE_FloatType tp -> Expr ids (FloatType tp) -> X86Generator st ids ()
setXMMreg_float_low r SSE_Single e = do
setLowBits (xmmOwner r) (bitcast fromSingle e)
setXMMreg_float_low r SSE_Double e = do
setLowBits (xmmOwner r) (bitcast fromDouble e)
-- ** Condition codes
@ -228,7 +297,8 @@ def_cmov_list =
r .= mux c y r_v
def_bswap :: InstructionDef
def_bswap = defUnaryLoc "bswap" $ \l -> do
def_bswap = defUnary "bswap" $ \_ val -> do
SomeBV l <- getSomeBVLocation val
v0 <- get l
l .= (bvUnvectorize (typeWidth l) $ reverse $ bvVectorize n8 v0)
@ -505,7 +575,8 @@ exec_cmp dst y = do
set_result_flags (dst_val .- y)
def_dec :: InstructionDef
def_dec = defUnaryLoc "dec" $ \dst -> do
def_dec = defUnary "dec" $ \_ dstVal -> do
SomeBV dst <- getSomeBVLocation dstVal
dst_val <- get dst
let v1 = bvLit (typeWidth dst_val) 1
-- Set overflow and arithmetic flags
@ -544,7 +615,8 @@ set_div_flags = do
-- | Unsigned (@div@ instruction) and signed (@idiv@ instruction) division.
def_div :: InstructionDef
def_div = defUnaryV "div" $ \d ->
def_div = defUnary "div" $ \_ val -> do
SomeBV d <- getSomeBVValue val
case typeWidth d of
n | Just Refl <- testEquality n n8 -> do
num <- get ax
@ -569,7 +641,8 @@ def_div = defUnaryV "div" $ \d ->
| otherwise -> fail "div: Unknown bit width"
def_idiv :: InstructionDef
def_idiv = defUnaryV "idiv" $ \d -> do
def_idiv = defUnary "idiv" $ \_ val -> do
SomeBV d <- getSomeBVValue val
set_div_flags
case typeWidth d of
n | Just Refl <- testEquality n n8 -> do
@ -601,7 +674,8 @@ def_hlt :: InstructionDef
def_hlt = defNullary "hlt" $ addArchTermStmt Hlt
def_inc :: InstructionDef
def_inc = defUnaryLoc "inc" $ \dst -> do
def_inc = defUnary "inc" $ \_ dstVal -> do
SomeBV dst <- getSomeBVLocation dstVal
-- Get current value stored in destination.
dst_val <- get dst
let y = bvLit (typeWidth dst_val) 1
@ -735,7 +809,8 @@ def_imul = defVariadic "imul" $ \_ vs ->
-- | Should be equiv to 0 - *l
def_neg :: InstructionDef
def_neg = defUnaryLoc "neg" $ \l -> do
def_neg = defUnary "neg" $ \_ val -> do
SomeBV l <- getSomeBVLocation val
v <- get l
cf_loc .= boolNot (is_zero v)
let r = bvNeg v
@ -1549,14 +1624,14 @@ def_lea = defBinary "lea" $ \_ loc (F.VoidMem ar) -> do
-- | FLD Load floating-point value
def_fld :: InstructionDef
def_fld = defUnary "fld" $ \_ v -> do
case v of
def_fld = defUnary "fld" $ \_ val -> do
case val of
F.FPMem32 ar -> do
l <- getBV32Addr ar
x87Push =<< evalArchFn . X87_Extend SSE_Single =<< eval =<< get l
v <- readMem ar singleMemRepr
x87Push . bitcast fromX87Float =<< evalArchFn (X87_Extend SSE_Single v)
F.FPMem64 ar -> do
l <- getBV64Addr ar
x87Push =<< evalArchFn . X87_Extend SSE_Double =<< eval =<< get l
v <- readMem ar doubleMemRepr
x87Push . bitcast fromX87Float =<< evalArchFn (X87_Extend SSE_Double v)
F.FPMem80 ar -> do
l <- getBV80Addr ar
x87Push =<< get l
@ -1570,14 +1645,16 @@ def_fstX mnem doPop = defUnary mnem $ \_ val -> do
v <- get (X87StackRegister 0)
case val of
F.FPMem32 ar -> do
l <- getBV32Addr ar
(l .=) =<< evalArchFn . X87_FST SSE_Single =<< eval v
l <- getBVAddress ar
extv <- evalArchFn . X87_FST SSE_Single =<< eval (bitcast toX87Float v)
MemoryAddr l singleMemRepr .= extv
F.FPMem64 ar -> do
l <- getBV64Addr ar
(l .=) =<< evalArchFn . X87_FST SSE_Double =<< eval v
l <- getBVAddress ar
extv <- evalArchFn . X87_FST SSE_Double =<< eval (bitcast toX87Float v)
MemoryAddr l doubleMemRepr .= extv
F.FPMem80 ar -> do
l <- getBV80Addr ar
l .= v
l <- getBVAddress ar
MemoryAddr l x87MemRepr .= v
F.X87Register n -> do
X87StackRegister n .= v
_ -> fail $ "Bad floating point argument."
@ -1606,19 +1683,19 @@ def_fstX mnem doPop = defUnary mnem $ \_ val -> do
type X87BinOp
= forall f
. f (FloatBVType X86_80Float)
-> f (FloatBVType X86_80Float)
-> X86PrimFn f (TupleType [FloatBVType X86_80Float, BoolType])
. f (FloatType X86_80Float)
-> f (FloatType X86_80Float)
-> X86PrimFn f (TupleType [FloatType X86_80Float, BoolType])
execX87BinOp :: X87BinOp
-> Location (Addr ids) (BVType 80)
-> Expr ids (BVType 80)
-> Expr ids (FloatType X86_80Float)
-> X86Generator st ids ()
execX87BinOp op loc expr1 = do
val0 <- eval =<< get loc
val0 <- eval . bitcast toX87Float =<< get loc
val1 <- eval expr1
res <- evalArchFn $ op val0 val1
loc .= app (TupleField knownRepr res P.index0)
loc .= bitcast fromX87Float (app (TupleField knownRepr res P.index0))
set_undefined c0_loc
c1_loc .= app (TupleField knownRepr res P.index1)
set_undefined c2_loc
@ -1632,17 +1709,17 @@ defX87BinaryInstruction mnem op =
case vs of
[F.FPMem32 addr] -> do
addr' <- getBVAddress addr
sVal <- eval =<< get (MemoryAddr addr' (floatMemRepr SingleFloatRepr))
sVal <- eval =<< get (MemoryAddr addr' singleMemRepr)
val <- evalArchFn $ X87_Extend SSE_Single sVal
execX87BinOp op (X87StackRegister 0) val
[F.FPMem64 addr] -> do
addr' <- getBVAddress addr
sVal <- eval =<< get (MemoryAddr addr' (floatMemRepr DoubleFloatRepr))
sVal <- eval =<< get (MemoryAddr addr' doubleMemRepr)
val <- evalArchFn $ X87_Extend SSE_Double sVal
execX87BinOp op (X87StackRegister 0) val
[F.X87Register x, F.X87Register y] -> do
val <- get (X87StackRegister y)
execX87BinOp op (X87StackRegister x) val
execX87BinOp op (X87StackRegister x) (bitcast toX87Float val)
_ -> do
fail $ mnem ++ "had unexpected arguments: " ++ show vs
@ -1654,7 +1731,7 @@ defX87PopInstruction mnem op =
case vs of
[F.X87Register x, F.X87Register 0] -> do
val <- get (X87StackRegister 0)
execX87BinOp op (X87StackRegister x) val
execX87BinOp op (X87StackRegister x) (bitcast toX87Float val)
x87Pop
_ -> do
fail $ mnem ++ "had unexpected arguments: " ++ show vs
@ -1823,21 +1900,21 @@ def_punpck suf f pieceSize = defBinaryLV ("punpck" ++ suf) $ \l v -> do
-- ** MMX Packed Arithmetic Instructions
def_padd :: (1 <= w) => String -> NatRepr w -> InstructionDef
def_padd suf w = defBinaryLV ("padd" ++ suf) $ \l v -> do
-- | This is used by MMX and SSE instructions
def_packed_binop :: (1 <= w)
=> String
-> NatRepr w
-> (forall ids . Expr ids (BVType w) -> Expr ids (BVType w) -> Expr ids (BVType w))
-> InstructionDef
def_packed_binop mnem w f = defBinaryLV mnem $ \l v -> do
v0 <- get l
l .= vectorize2 w (.+) v0 v
l .= vectorize2 w f v0 v
-- PADDSB Add packed signed byte integers with signed saturation
-- PADDSW Add packed signed word integers with signed saturation
-- PADDUSB Add packed unsigned byte integers with unsigned saturation
-- PADDUSW Add packed unsigned word integers with unsigned saturation
def_psub :: (1 <= w) => String -> NatRepr w -> InstructionDef
def_psub suf w = defBinaryLV ("psub" ++ suf) $ \l v -> do
v0 <- get l
l .= vectorize2 w (.-) v0 v
-- PSUBSB Subtract packed signed byte integers with signed saturation
-- PSUBSW Subtract packed signed word integers with signed saturation
-- PSUBUSB Subtract packed unsigned byte integers with unsigned saturation
@ -1854,13 +1931,8 @@ def_pcmp :: 1 <= o
-> (forall ids . BVExpr ids o -> BVExpr ids o -> Expr ids BoolType)
-> NatRepr o
-> InstructionDef
def_pcmp nm op sz =
defBinaryLV nm $ \l v -> do
v0 <- get l
let chkHighLow d s = mux (d `op` s)
(bvLit (typeWidth d) (negate 1))
(bvLit (typeWidth d) 0)
l .= vectorize2 sz chkHighLow v0 v
def_pcmp nm op sz = do
def_packed_binop nm sz (\d s -> mux (op d s) (bvLit sz (negate 1)) (bvLit sz 0))
-- ** MMX Logical Instructions
@ -1964,15 +2036,15 @@ def_movss = defBinary "movss" $ \_ v1 v2 -> do
_ ->
fail $ "Unexpected arguments in FlexdisMatcher.movss: " ++ show v1 ++ ", " ++ show v2
def_pshufb :: InstructionDef
def_pshufb = defBinary "pshufb" $ \_ f_d f_s -> do
case (f_d, f_s) of
(F.XMMReg {}, F.XMMReg {}) -> do
loc_d <- getBVLocation f_d n128
d_val <- eval =<< get loc_d
s_val <- eval =<< getBVValue f_s n128
r <- evalArchFn $ PShufb SIMD_128 d_val s_val
loc_d .= r
(F.XMMReg d, F.XMMReg s) -> do
dVal <- eval . bitcast toXMMBytes . bvTrunc' n128 =<< getReg (xmmOwner d)
sVal <- eval . bitcast toXMMBytes . bvTrunc' n128 =<< getReg (xmmOwner s)
r <- evalArchFn $ PShufb SIMDByteCount_XMM dVal sVal
setLowBits (xmmOwner d) (bitcast fromXMMBytes r)
_ -> do
fail $ "pshufb only supports 2 XMM registers as arguments."
@ -2036,12 +2108,11 @@ def_movlps = defBinary "movlps" $ \_ x y -> do
-- and applies a function that updates the low 64-bits of the first argument.
def_xmm_ss :: SSE_Op -> InstructionDef
def_xmm_ss f =
defBinary (sseOpName f ++ "ss") $ \_ loc val -> do
d <- getXMM loc
y <- eval =<< get =<< getXMM_mr_low32 val
x <- eval =<< get (xmm_low32 d)
res <- evalArchFn $ SSE_VectorOp f n1 SSE_Single x y
xmm_low32 d .= res
defBinary (sseOpName f ++ "ss") $ \_ (F.XMMReg loc) val -> do
x <- getXMMreg_float_low loc SSE_Single
y <- getXMM_float_low val SSE_Single
res <- evalArchFn $ SSE_UnaryOp f SSE_Single x y
setXMMreg_float_low loc SSE_Single res
-- ADDSS Add scalar single-precision floating-point values
def_addss :: InstructionDef
@ -2063,12 +2134,11 @@ def_divss = def_xmm_ss SSE_Div
-- and applies a function that updates the register.
def_xmm_packed :: SSE_Op -> InstructionDef
def_xmm_packed f =
defBinary (sseOpName f ++ "ps") $ \_ loc val -> do
d <- xmm_sse <$> getXMM loc
x <- eval =<< get d
y <- eval =<< get =<< getXMM_mr val
defBinary (sseOpName f ++ "ps") $ \_ (F.XMMReg loc) val -> do
x <- getXMMreg_sv loc
y <- getXMM_sv val
res <- evalArchFn $ SSE_VectorOp f n4 SSE_Single x y
d .= res
setXMMreg_sv loc res
-- | ADDPS Add packed single-precision floating-point values
def_addps :: InstructionDef
@ -2092,8 +2162,12 @@ def_divps = def_xmm_packed SSE_Div
-- SQRTPS Compute square roots of packed single-precision floating-point values
-- |SQRTSS Compute square root of scalar single-precision floating-point values
def_sqrtss :: InstructionDef
def_sqrtss = def_xmm_ss SSE_Sqrt
def_sqrts :: String -> SSE_FloatType ftp -> InstructionDef
def_sqrts mnem ftp =
defBinary mnem $ \_ (F.XMMReg loc) val -> do
y <- getXMM_float_low val ftp
res <- evalArchFn $ SSE_Sqrt ftp y
setXMMreg_float_low loc ftp res
-- RSQRTPS Compute reciprocals of square roots of packed single-precision floating-point values
-- RSQRTSS Compute reciprocal of square root of scalar single-precision floating-point values
@ -2122,8 +2196,8 @@ def_ucomisd :: InstructionDef
-- Invalid (if SNaN operands), Denormal.
def_ucomisd =
defBinary "ucomisd" $ \_ xv yv -> do
x <- eval =<< get =<< getXMM_mr_low64 xv
y <- eval =<< get =<< getXMM_mr_low64 yv
x <- getXMM_float_low xv SSE_Double
y <- getXMM_float_low yv SSE_Double
res <- evalArchFn (SSE_UCOMIS SSE_Double x y)
zf_loc .= app (TupleField knownRepr res P.index0)
pf_loc .= app (TupleField knownRepr res P.index1)
@ -2141,8 +2215,8 @@ def_ucomiss :: InstructionDef
-- Invalid (if SNaN operands), Denormal.
def_ucomiss =
defBinary "ucomiss" $ \_ xv yv -> do
x <- eval =<< get =<< getXMM_mr_low32 xv
y <- eval =<< get =<< getXMM_mr_low32 yv
x <- getXMM_float_low xv SSE_Single
y <- getXMM_float_low yv SSE_Single
res <- evalArchFn (SSE_UCOMIS SSE_Single x y)
zf_loc .= app (TupleField knownRepr res P.index0)
pf_loc .= app (TupleField knownRepr res P.index1)
@ -2153,29 +2227,34 @@ def_ucomiss =
-- *** SSE Logical Instructions
exec_bifpx :: 1 <= elsz =>
(Expr ids (BVType elsz) -> Expr ids (BVType elsz) -> Expr ids (BVType elsz))
def_bifpx :: forall elsz
. 1 <= elsz
=> String
-> (forall ids . Expr ids (BVType elsz) -> Expr ids (BVType elsz) -> Expr ids (BVType elsz))
-> NatRepr elsz
-> Location (Addr ids) XMMType
-> Expr ids XMMType
-> X86Generator st ids ()
exec_bifpx f elsz l v = fmap_loc l $ \lv -> (vectorize2 elsz) (f) lv v
-> InstructionDef
def_bifpx mnem f elsz =
defBinary mnem $ \_ loc val -> do
l <- getBVLocation loc n128
v <- getBVValue val n128
fmap_loc l $ \lv ->
vectorize2 elsz f lv v
-- | ANDPS Perform bitwise logical AND of packed single-precision floating-point values
def_andps :: InstructionDef
def_andps = defBinaryKnown "andps" $ exec_bifpx (.&.) n32
def_andps = def_bifpx "andps" (.&.) n32
-- ANDNPS Perform bitwise logical AND NOT of packed single-precision floating-point values
-- | ANDNPS Perform bitwise logical AND NOT of packed single-precision floating-point values
def_andnps :: InstructionDef
def_andnps = defBinaryKnown "andnps" $ exec_bifpx (\a b -> bvComplement $ (.&.) a b) n32
def_andnps = def_bifpx "andnps" (\a b -> bvComplement $ (.&.) a b) n32
-- | ORPS Perform bitwise logical OR of packed single-precision floating-point values
def_orps :: InstructionDef
def_orps = defBinaryKnown "orps" $ exec_bifpx (.|.) n32
def_orps = def_bifpx "orps" (.|.) n32
-- | XORPS Perform bitwise logical XOR of packed single-precision floating-point values
def_xorps :: InstructionDef
def_xorps = defBinaryKnown "xorps" $ exec_bifpx bvXor n32
def_xorps = def_bifpx "xorps" bvXor n32
-- *** SSE Shuffle and Unpack Instructions
@ -2199,17 +2278,16 @@ def_unpcklps = defBinaryKnown "unpcklps" exec
-- CVTSI2SS Convert doubleword integer to scalar single-precision floating-point value
def_cvtsi2sX :: String -> SSE_FloatType tp -> InstructionDef
def_cvtsi2sX mnem tp =
defBinary mnem $ \_ loc val -> do
defBinary mnem $ \_ (F.XMMReg loc) val -> do
-- Loc is RG_XMM_reg
-- val is "OpType ModRM_rm YSize"
d <- getXMM loc
ev <- getRM32_RM64 val
-- Read second argument value and coerce to single precision float.
r <-
case ev of
Left v -> evalArchFn . SSE_CVTSI2SX tp n32 =<< eval =<< get v
Right v -> evalArchFn . SSE_CVTSI2SX tp n64 =<< eval =<< get v
xmm_low d tp .= r
setXMMreg_float_low loc tp r
-- CVTPI2PS Convert packed doubleword integers to packed single-precision floating-point values
@ -2344,12 +2422,11 @@ def_xmm_sd :: SSE_Op
-- ^ Binary operation
-> InstructionDef
def_xmm_sd f =
defBinary (sseOpName f ++ "sd") $ \_ loc val -> do
d <- getXMM loc
y <- eval =<< get =<< getXMM_mr_low64 val
x <- eval =<< get (xmm_low64 d)
res <- evalArchFn $ SSE_VectorOp f n1 SSE_Double x y
xmm_low64 d .= res
defBinary (sseOpName f ++ "sd") $ \_ (F.XMMReg loc) val -> do
x <- getXMMreg_float_low loc SSE_Double
y <- getXMM_float_low val SSE_Double
res <- evalArchFn $ SSE_UnaryOp f SSE_Double x y
setXMMreg_float_low loc SSE_Double res
-- | ADDSD Add scalar double precision floating-point values
def_addsd :: InstructionDef
@ -2375,10 +2452,6 @@ def_divsd = def_xmm_sd SSE_Div
-- SQRTPD Compute packed square roots of packed double-precision floating-point values
-- | SQRTSD Compute scalar square root of scalar double-precision floating-point values
def_sqrtsd :: InstructionDef
def_sqrtsd = def_xmm_sd SSE_Sqrt
-- MAXPD Return maximum packed double-precision floating-point values
-- MAXSD Return maximum scalar double-precision floating-point values
-- MINPD Return minimum packed double-precision floating-point values
@ -2388,12 +2461,12 @@ def_sqrtsd = def_xmm_sd SSE_Sqrt
-- | ANDPD Perform bitwise logical AND of packed double-precision floating-point values
def_andpd :: InstructionDef
def_andpd = defBinaryKnown "andpd" $ exec_bifpx (.&.) n64
def_andpd = def_bifpx "andpd" (.&.) n64
-- ANDNPD Perform bitwise logical AND NOT of packed double-precision floating-point values
-- | ORPD Perform bitwise logical OR of packed double-precision floating-point values
def_orpd :: InstructionDef
def_orpd = defBinaryKnown "orpd" $ exec_bifpx (.|.) n64
def_orpd = def_bifpx "orpd" (.|.) n64
-- XORPD Perform bitwise logical XOR of packed double-precision floating-point values
@ -2410,16 +2483,20 @@ def_xorpd =
-- | CMPSD Compare scalar double-precision floating-point values
def_cmpsX :: String -> SSE_FloatType tp -> InstructionDef
def_cmpsX mnem tp =
defTernary mnem $ \_ loc f_val (F.ByteImm imm) -> do
l <- getXMM loc
v <- eval =<< get =<< getXMM_mr_low f_val tp
defTernary mnem $ \_ (F.XMMReg loc) f_val (F.ByteImm imm) -> do
f <-
case lookupSSECmp imm of
Just f -> pure f
Nothing -> fail $ mnem ++ " had unsupported operator type " ++ show imm ++ "."
lv <- eval =<< get (xmm_low l tp)
lv <- getXMMreg_float_low loc tp
v <- getXMM_float_low f_val tp
res <- evalArchFn $ SSE_CMPSX f tp lv v
xmm_low l tp .= res
let w = floatInfoBits (typeRepr tp)
case testLeq n1 w of
Nothing ->
error "Unexpected width"
Just LeqProof ->
xmm_low loc tp .= mux res (bvLit w (-1)) (bvLit w 0)
-- COMISD Perform ordered comparison of scalar double-precision floating-point values and set flags in EFLAGS register
@ -2445,25 +2522,23 @@ def_cmpsX mnem tp =
-- | CVTSS2SD Convert scalar single-precision floating-point values to
-- scalar double-precision floating-point values
def_cvtss2sd :: InstructionDef
def_cvtss2sd = defBinary "cvtss2sd" $ \_ loc val -> do
r <- getXMM loc
v <- eval =<< get =<< getXMM_mr_low32 val
(xmm_low64 r .=) =<< evalArchFn (SSE_CVTSS2SD v)
def_cvtss2sd = defBinary "cvtss2sd" $ \_ (F.XMMReg loc) val -> do
v <- getXMM_float_low val SSE_Single
setXMMreg_float_low loc SSE_Double =<< evalArchFn (SSE_CVTSS2SD v)
-- | CVTSD2SS Convert scalar double-precision floating-point values to
-- scalar single-precision floating-point values
def_cvtsd2ss :: InstructionDef
def_cvtsd2ss = defBinary "cvtsd2ss" $ \_ loc val -> do
r <- getXMM loc
v <- eval =<< get =<< getXMM_mr_low64 val
(xmm_low32 r .=) =<< evalArchFn (SSE_CVTSD2SS v)
def_cvtsd2ss = defBinary "cvtsd2ss" $ \_ (F.XMMReg loc) val -> do
v <- getXMM_float_low val SSE_Double
setXMMreg_float_low loc SSE_Single =<< evalArchFn (SSE_CVTSD2SS v)
-- CVTSD2SI Convert scalar double-precision floating-point values to a doubleword integer
def_cvttsX2si :: String -> SSE_FloatType tp -> InstructionDef
def_cvttsX2si mnem tp =
defBinary mnem $ \_ loc val -> do
v <- eval =<< get =<< getXMM_mr_low val tp
v <- getXMM_float_low val tp
case loc of
F.DWordReg r ->
(reg32Loc r .=) =<< evalArchFn (SSE_CVTTSX2SI n32 tp v)
@ -2785,10 +2860,14 @@ all_instructions =
, def_inc
, def_leave
, def_mov
, defUnaryV "mul" $ exec_mul
, defUnary "mul" $ \_ val -> do
SomeBV v <- getSomeBVValue val
exec_mul v
, def_neg
, defNullary "nop" $ return ()
, defUnaryLoc "not" $ \l -> modify l bvComplement
, defUnary "not" $ \_ val -> do
SomeBV l <- getSomeBVLocation val
modify l bvComplement
, defBinaryLV "or" $ exec_or
, defNullary "pause" $ return ()
, def_pop
@ -2833,15 +2912,14 @@ all_instructions =
, def_punpck "ldq" snd n32
, def_punpck "lqdq" snd n64
, def_padd "b" n8
, def_padd "w" n16
, def_padd "d" n32
-- FIXME: Can "paddq" can also take 64 bit values?
, def_padd "q" n64
, def_packed_binop "paddb" n8 (.+)
, def_packed_binop "paddw" n16 (.+)
, def_packed_binop "paddd" n32 (.+)
, def_packed_binop "paddq" n64 (.+)
, def_psub "b" n8
, def_psub "w" n16
, def_psub "d" n32
, def_packed_binop "psubb" n8 (.-)
, def_packed_binop "psubw" n16 (.-)
, def_packed_binop "psubd" n32 (.-)
, def_pcmp "pcmpeqb" (.=.) n8
, def_pcmp "pcmpeqw" (.=.) n16
@ -2871,8 +2949,8 @@ all_instructions =
, def_mulss
, def_divss
, def_minss
, def_sqrtss
, def_sqrtsd
, def_sqrts "sqrtss" SSE_Single
, def_sqrts "sqrtsd" SSE_Double
, def_minps
, def_maxss
, def_maxps

1
x86_symbolic/macaw-x86-symbolic.cabal
View File

@ -19,6 +19,7 @@ library
macaw-x86,
mtl,
parameterized-utils,
vector,
what4 >= 0.4
hs-source-dirs: src
default-language: Haskell2010

270
x86_symbolic/src/Data/Macaw/X86/Crucible.hs
View File

@ -27,11 +27,9 @@ module Data.Macaw.X86.Crucible
, liftAtomMap
, liftAtomTrav
, liftAtomIn
) where
-- type SymInterpretedFloat sym fi = SymExpr sym (SymInterpretedFloatType sym fi)
import Control.Lens ((^.))
import Control.Monad
import Data.Bits hiding (xor)
@ -41,6 +39,7 @@ import Data.Parameterized.NatRepr
import Data.Parameterized.Utils.Endian (Endian(..))
import qualified Data.Parameterized.Vector as PV
import Data.Semigroup
import qualified Data.Vector as DV
import Data.Word (Word8)
import GHC.TypeLits (KnownNat)
import Text.PrettyPrint.ANSI.Leijen hiding ( (<$>), (<>), empty )
@ -71,13 +70,13 @@ import Lang.Crucible.LLVM.MemModel
)
import qualified Data.Macaw.CFG.Core as M
import qualified Data.Macaw.CFG.Core as MC
import qualified Data.Macaw.Memory as M
import qualified Data.Macaw.Types as M
import Data.Macaw.Symbolic
import Data.Macaw.Symbolic.Backend
import qualified Data.Macaw.Types as M
import qualified Data.Macaw.X86 as M
import qualified Data.Macaw.X86.ArchTypes as M
import qualified Data.Macaw.CFG.Core as MC
import Prelude
@ -85,11 +84,12 @@ import Prelude
type S sym rtp bs r ctx =
CrucibleState (MacawSimulatorState sym) sym (MacawExt M.X86_64) rtp bs r ctx
funcSemantics ::
(IsSymInterface sym, ToCrucibleType mt ~ t) =>
SymFuns sym ->
M.X86PrimFn (AtomWrapper (RegEntry sym)) mt ->
S sym rtp bs r ctx -> IO (RegValue sym t, S sym rtp bs r ctx)
funcSemantics
:: (IsSymInterface sym, ToCrucibleType mt ~ t)
=> SymFuns sym
-> M.X86PrimFn (AtomWrapper (RegEntry sym)) mt
-> S sym rtp bs r ctx
-> IO (RegValue sym t, S sym rtp bs r ctx)
funcSemantics fs x s = do let sym = Sym { symIface = s^.stateSymInterface
, symTys = s^.stateIntrinsicTypes
, symFuns = fs
@ -134,35 +134,29 @@ stmtSemantics _sym_funs global_var_mem globals stmt state = do
let mem_repr = M.repValSizeMemRepr val_size
curr_dest_ptr <- ptrAdd sym knownNat (regValue dest) offset
curr_src_ptr <- ptrAdd sym knownNat (regValue src) offset
(val, after_read_state) <- doReadMem
acc_state
global_var_mem
globals
M.Addr64
mem_repr
(RegEntry knownRepr curr_src_ptr)
(_, after_write_state) <- doWriteMem
after_read_state
global_var_mem
globals
M.Addr64
mem_repr
(RegEntry knownRepr curr_dest_ptr)
(RegEntry (typeToCrucible $ M.typeRepr mem_repr) val)
return after_write_state
-- Get simulator and memory
mem <- getMem acc_state global_var_mem
-- Resolve source pointer
resolvedSrcPtr <- tryGlobPtr sym mem globals curr_src_ptr
-- Read resolvePtr
val <- doReadMem sym mem M.Addr64 mem_repr resolvedSrcPtr
-- Resolve destination pointer
resolvedDestPtr <- tryGlobPtr sym mem globals curr_dest_ptr
afterWriteMem <- doWriteMem sym mem M.Addr64 mem_repr resolvedDestPtr val
-- Update the final state
pure $! setMem acc_state global_var_mem afterWriteMem
M.RepStos val_size (AtomWrapper dest) (AtomWrapper val) count dir ->
withConcreteCountAndDir state val_size count dir $ \acc_state offset -> do
let mem_repr = M.repValSizeMemRepr val_size
curr_dest_ptr <- ptrAdd sym knownNat (regValue dest) offset
(_, after_write_state) <- doWriteMem
acc_state
global_var_mem
globals
M.Addr64
mem_repr
(RegEntry knownRepr curr_dest_ptr)
val
return after_write_state
let mem_repr = M.repValSizeMemRepr val_size
-- Get simulator and memory
mem <- getMem acc_state global_var_mem
-- Resolve address to write to.
curr_dest_ptr <- ptrAdd sym knownNat (regValue dest) offset
resolvedDestPtr <- tryGlobPtr sym mem globals curr_dest_ptr
-- Perform write
afterWriteMem <- doWriteMem sym mem M.Addr64 mem_repr resolvedDestPtr (regValue val)
-- Update the final state
pure $! setMem acc_state global_var_mem afterWriteMem
_ -> error $
"Symbolic execution semantics for x86 statement are not implemented yet: "
<> (show $ MC.ppArchStmt (liftAtomIn (pretty . regType)) stmt)
@ -216,10 +210,11 @@ newSymFuns s =
Left _ -> fail "Invalid symbol name"
-- | Semantics for operations that do not affect Crucible's state directly.
pureSem :: (IsSymInterface sym) =>
Sym sym {- ^ Handle to the simulator -} ->
M.X86PrimFn (AtomWrapper (RegEntry sym)) mt {- ^ Instruction -} ->
IO (RegValue sym (ToCrucibleType mt)) -- ^ Resulting value
pureSem :: forall sym mt
. IsSymInterface sym
=> Sym sym {- ^ Handle to the simulator -}
-> M.X86PrimFn (AtomWrapper (RegEntry sym)) mt {- ^ Instruction -}
-> IO (RegValue sym (ToCrucibleType mt)) -- ^ Resulting value
pureSem sym fn = do
let symi = (symIface sym)
case fn of
@ -245,84 +240,72 @@ pureSem sym fn = do
M.X87_FST {} -> error "X87_FST"
M.VExtractF128 {} -> error "VExtractF128"
M.SSE_VectorOp op n (tp :: M.SSE_FloatType (M.BVType w)) x y -> do
let w = M.typeWidth tp
vecOp2M sym BigEndian (natMultiply n w) w x y $ V.zipWithM $ \x' y' -> do
x'' <- toValFloat' sym tp x'
y'' <- toValFloat' sym tp y'
fromValFloat' symi tp =<< case op of
M.SSE_Add ->
iFloatAdd @_ @(FloatInfoFromSSEType (M.BVType w)) symi RNE x'' y''
M.SSE_Sub ->
iFloatSub @_ @(FloatInfoFromSSEType (M.BVType w)) symi RNE x'' y''
M.SSE_Mul ->
iFloatMul @_ @(FloatInfoFromSSEType (M.BVType w)) symi RNE x'' y''
M.SSE_Div ->
iFloatDiv @_ @(FloatInfoFromSSEType (M.BVType w)) symi RNE x'' y''
M.SSE_Min ->
iFloatMin @_ @(FloatInfoFromSSEType (M.BVType w)) symi x'' y''
M.SSE_Max ->
iFloatMax @_ @(FloatInfoFromSSEType (M.BVType w)) symi x'' y''
M.SSE_Sqrt ->
iFloatSqrt @_ @(FloatInfoFromSSEType (M.BVType w)) symi RTP x''
M.SSE_CMPSX op (tp :: M.SSE_FloatType tp) x y -> do
x' <- toValFloat symi tp x
y' <- toValFloat symi tp y
res <- case op of
M.EQ_OQ -> iFloatFpEq @_ @(FloatInfoFromSSEType tp) symi x' y'
M.LT_OS -> iFloatLt @_ @(FloatInfoFromSSEType tp) symi x' y'
M.LE_OS -> iFloatLe @_ @(FloatInfoFromSSEType tp) symi x' y'
M.SSE_UnaryOp op (_tp :: M.SSE_FloatType ftp) (AtomWrapper x) (AtomWrapper y) -> do
let f = case op of
M.SSE_Add -> iFloatAdd @_ @(ToCrucibleFloatInfo ftp) symi RNE
M.SSE_Sub -> iFloatSub @_ @(ToCrucibleFloatInfo ftp) symi RNE
M.SSE_Mul -> iFloatMul @_ @(ToCrucibleFloatInfo ftp) symi RNE
M.SSE_Div -> iFloatDiv @_ @(ToCrucibleFloatInfo ftp) symi RNE
M.SSE_Min -> iFloatMin @_ @(ToCrucibleFloatInfo ftp) symi
M.SSE_Max -> iFloatMax @_ @(ToCrucibleFloatInfo ftp) symi
f (regValue x) (regValue y)
M.SSE_VectorOp op _n (_tp :: M.SSE_FloatType ftp) (AtomWrapper x) (AtomWrapper y) -> do
let f = case op of
M.SSE_Add -> iFloatAdd @_ @(ToCrucibleFloatInfo ftp) symi RNE
M.SSE_Sub -> iFloatSub @_ @(ToCrucibleFloatInfo ftp) symi RNE
M.SSE_Mul -> iFloatMul @_ @(ToCrucibleFloatInfo ftp) symi RNE
M.SSE_Div -> iFloatDiv @_ @(ToCrucibleFloatInfo ftp) symi RNE
M.SSE_Min -> iFloatMin @_ @(ToCrucibleFloatInfo ftp) symi
M.SSE_Max -> iFloatMax @_ @(ToCrucibleFloatInfo ftp) symi
DV.zipWithM f (regValue x) (regValue y)
M.SSE_Sqrt (_tp :: M.SSE_FloatType ftp) (AtomWrapper x) -> do
iFloatSqrt @_ @(ToCrucibleFloatInfo ftp) symi RTP (regValue x)
M.SSE_CMPSX op (_tp :: M.SSE_FloatType ftp) (AtomWrapper x) (AtomWrapper y) -> do
let x' = regValue x
let y' = regValue y
case op of
M.EQ_OQ -> iFloatFpEq @_ @(ToCrucibleFloatInfo ftp) symi x' y'
M.LT_OS -> iFloatLt @_ @(ToCrucibleFloatInfo ftp) symi x' y'
M.LE_OS -> iFloatLe @_ @(ToCrucibleFloatInfo ftp) symi x' y'
M.UNORD_Q -> do
x_is_nan <- iFloatIsNaN @_ @(FloatInfoFromSSEType tp) symi x'
y_is_nan <- iFloatIsNaN @_ @(FloatInfoFromSSEType tp) symi y'
x_is_nan <- iFloatIsNaN @_ @(ToCrucibleFloatInfo ftp) symi x'
y_is_nan <- iFloatIsNaN @_ @(ToCrucibleFloatInfo ftp) symi y'
orPred symi x_is_nan y_is_nan
M.NEQ_UQ ->
notPred symi =<< iFloatFpEq @_ @(FloatInfoFromSSEType tp) symi x' y'
notPred symi =<< iFloatFpEq @_ @(ToCrucibleFloatInfo ftp) symi x' y'
M.NLT_US ->
notPred symi =<< iFloatLt @_ @(FloatInfoFromSSEType tp) symi x' y'
notPred symi =<< iFloatLt @_ @(ToCrucibleFloatInfo ftp) symi x' y'
M.NLE_US ->
notPred symi =<< iFloatLe @_ @(FloatInfoFromSSEType tp) symi x' y'
notPred symi =<< iFloatLe @_ @(ToCrucibleFloatInfo ftp) symi x' y'
M.ORD_Q -> do
x_is_nan <- iFloatIsNaN @_ @(FloatInfoFromSSEType tp) symi x'
y_is_nan <- iFloatIsNaN @_ @(FloatInfoFromSSEType tp) symi y'
x_is_nan <- iFloatIsNaN @_ @(ToCrucibleFloatInfo ftp) symi x'
y_is_nan <- iFloatIsNaN @_ @(ToCrucibleFloatInfo ftp) symi y'
notPred symi =<< orPred symi x_is_nan y_is_nan
case tp of
M.SSE_Single -> do
zeros <- minUnsignedBV symi knownNat
ones <- maxUnsignedBV symi knownNat
llvmPointer_bv symi =<< bvIte symi res ones zeros
M.SSE_Double -> do
zeros <- minUnsignedBV symi knownNat
ones <- maxUnsignedBV symi knownNat
llvmPointer_bv symi =<< bvIte symi res ones zeros
M.SSE_UCOMIS (tp :: M.SSE_FloatType tp) x y -> do
x' <- toValFloat symi tp x
y' <- toValFloat symi tp y
is_eq <- iFloatFpEq @_ @(FloatInfoFromSSEType tp) symi x' y'
is_lt <- iFloatLt @_ @(FloatInfoFromSSEType tp) symi x' y'
x_is_nan <- iFloatIsNaN @_ @(FloatInfoFromSSEType tp) symi x'
y_is_nan <- iFloatIsNaN @_ @(FloatInfoFromSSEType tp) symi y'
M.SSE_UCOMIS (_tp :: M.SSE_FloatType ftp) (AtomWrapper x) (AtomWrapper y) -> do
let x' = regValue x
let y' = regValue y
is_eq <- iFloatFpEq @_ @(ToCrucibleFloatInfo ftp) symi x' y'
is_lt <- iFloatLt @_ @(ToCrucibleFloatInfo ftp) symi x' y'
x_is_nan <- iFloatIsNaN @_ @(ToCrucibleFloatInfo ftp) symi x'
y_is_nan <- iFloatIsNaN @_ @(ToCrucibleFloatInfo ftp) symi y'
is_unord <- orPred symi x_is_nan y_is_nan
zf <- orPred symi is_eq is_unord
cf <- orPred symi is_lt is_unord
let pf = is_unord
return $ empty `extend` (RV zf) `extend` (RV pf) `extend` (RV cf)
M.SSE_CVTSS2SD x ->
fromValFloat symi M.SSE_Double
=<< iFloatCast @_ @DoubleFloat @SingleFloat symi knownRepr RNE
=<< toValFloat symi M.SSE_Single x
M.SSE_CVTSD2SS x ->
fromValFloat symi M.SSE_Single
=<< iFloatCast @_ @SingleFloat @DoubleFloat symi knownRepr RNE
=<< toValFloat symi M.SSE_Double x
M.SSE_CVTSS2SD (AtomWrapper x) ->
iFloatCast @_ @DoubleFloat @SingleFloat symi knownRepr RNE (regValue x)
M.SSE_CVTSD2SS (AtomWrapper x) ->
iFloatCast @_ @SingleFloat @DoubleFloat symi knownRepr RNE (regValue x)
M.SSE_CVTSI2SX tp _ x ->
fromValFloat symi tp
=<< iSBVToFloat symi (floatInfoFromSSEType tp) RNE
iSBVToFloat symi (floatInfoFromSSEType tp) RNE
=<< toValBV symi x
M.SSE_CVTTSX2SI w (tp :: M.SSE_FloatType tp) x ->
M.SSE_CVTTSX2SI w (_ :: M.SSE_FloatType ftp) (AtomWrapper x) ->
llvmPointer_bv symi
=<< iFloatToSBV @_ @_ @(FloatInfoFromSSEType tp) symi w RTZ
=<< toValFloat symi tp x
=<< iFloatToSBV @_ @_ @(ToCrucibleFloatInfo ftp) symi w RTZ (regValue x)
M.EvenParity x0 ->
do x <- getBitVal (symIface sym) x0
@ -405,10 +388,6 @@ pureSem sym fn = do
| otherwise -> fail "Unexpecte size for AESEncLast"
M.PointwiseShiftL elNum elSz shSz bits amt ->
do amt' <- getBitVal (symIface sym) amt
vecOp1 sym LittleEndian (natMultiply elNum elSz) elSz bits $ \xs ->
@ -628,27 +607,6 @@ vecOp2 sym endian totLen elLen x y f =
unpack2 (symIface sym) endian totLen elLen x y $ \u v ->
llvmPointer_bv (symIface sym) =<< evalE sym (V.toBV endian elLen (f u v))
vecOp2M
:: (IsSymInterface sym, 1 <= c)
=> Sym sym {- ^ Simulator -}
-> Endian {- ^ How to split-up the bit-vector -}
-> NatRepr w {- ^ Total width of the bit-vector -}
-> NatRepr c {- ^ Width of individual elements -}
-> AtomWrapper (RegEntry sym) (M.BVType w) {- ^ Input value 1 -}
-> AtomWrapper (RegEntry sym) (M.BVType w) {- ^ Input value 2 -}
-> ( forall n
. (1 <= n, (n * c) ~ w)
=> V.Vector n (E sym (BVType c))
-> V.Vector n (E sym (BVType c))
-> IO (V.Vector n (E sym (BVType c)))
) {- ^ Definition of operation -}
-> IO (RegValue sym (LLVMPointerType w)) -- ^ The final result.
vecOp2M sym endian totLen elLen x y f =
unpack2 (symIface sym) endian totLen elLen x y $ \u v ->
llvmPointer_bv (symIface sym)
=<< evalE sym
=<< (V.toBV endian elLen <$> f u v)
bitOp2 :: (IsSymInterface sym) =>
Sym sym {- ^ The simulator -} ->
AtomWrapper (RegEntry sym) (M.BVType w) {- ^ Input 1 -} ->
@ -728,63 +686,11 @@ type family FloatInfoFromSSEType (tp :: M.Type) :: FloatInfo where
FloatInfoFromSSEType (M.BVType 64) = DoubleFloat
floatInfoFromSSEType
:: M.SSE_FloatType tp -> FloatInfoRepr (FloatInfoFromSSEType tp)
:: M.SSE_FloatType tp -> FloatInfoRepr (ToCrucibleFloatInfo tp)
floatInfoFromSSEType = \case
M.SSE_Single -> knownRepr
M.SSE_Double -> knownRepr
toValFloat
:: IsSymInterface sym
=> sym
-> M.SSE_FloatType tp
-> AtomWrapper (RegEntry sym) tp
-> IO (RegValue sym (FloatType (FloatInfoFromSSEType tp)))
toValFloat sym tp (AtomWrapper x) =
case tp of
M.SSE_Single ->
iFloatFromBinary sym SingleFloatRepr =<< projectLLVM_bv sym (regValue x)
M.SSE_Double ->
iFloatFromBinary sym DoubleFloatRepr =<< projectLLVM_bv sym (regValue x)
toValFloat'
:: IsSymInterface sym
=> Sym sym
-> M.SSE_FloatType (M.BVType w)
-> E sym (BVType w)
-> IO (RegValue sym (FloatType (FloatInfoFromSSEType (M.BVType w))))
toValFloat' sym tp x =
case tp of
M.SSE_Single ->
iFloatFromBinary (symIface sym) SingleFloatRepr =<< evalE sym x
M.SSE_Double ->
iFloatFromBinary (symIface sym) DoubleFloatRepr =<< evalE sym x
fromValFloat
:: IsSymInterface sym
=> sym
-> M.SSE_FloatType tp
-> RegValue sym (FloatType (FloatInfoFromSSEType tp))
-> IO (RegValue sym (ToCrucibleType tp))
fromValFloat sym tp x =
case tp of
M.SSE_Single -> llvmPointer_bv sym =<< iFloatToBinary sym SingleFloatRepr x
M.SSE_Double -> llvmPointer_bv sym =<< iFloatToBinary sym DoubleFloatRepr x
fromValFloat'
:: IsSymInterface sym
=> sym
-> M.SSE_FloatType (M.BVType w)
-> RegValue sym (FloatType (FloatInfoFromSSEType (M.BVType w)))
-> IO (E sym (BVType w))
fromValFloat' sym tp x =
case tp of
M.SSE_Single -> ValBV knownNat <$> iFloatToBinary sym SingleFloatRepr x
M.SSE_Double -> ValBV knownNat <$> iFloatToBinary sym DoubleFloatRepr x
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
-- A small functor that allows mixing of values and Crucible expressions.

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

@ -216,6 +216,7 @@ freshValue sym str w ty =
WI.freshConstant sym nm C.BaseBoolRepr
M.TupleTypeRepr {} -> crash [ "Unexpected symbolic tuple:", show str ]
M.VecTypeRepr {} -> crash [ "Unexpected symbolic vector:", show str ]
where
symName x =
@ -229,12 +230,6 @@ freshValue sym str w ty =
y : ys -> fail $ unlines $ ("[freshX86Reg] " ++ y)
: [ "*** " ++ z | z <- ys ]
------------------------------------------------------------------------
------------------------------------------------------------------------
-- Other X86 specific