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

Begin cleaning up floating point and x86-specific functions.

Browse Source
This commit is contained in:
Joe Hendrix 2017-12-05 13:31:12 -08:00
parent 716de707c2
commit 4d5b90e285
No known key found for this signature in database
GPG Key ID: 8DFA5FF784098C4F
17 changed files with 306 additions and 238 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
base/src/Data/Macaw/AbsDomain/AbsState.hs
View File

@ -339,6 +339,10 @@ isEmpty _ = False
-------------------------------------------------------------------------------
-- Joining abstract values
instance MemWidth w => AbsDomain (AbsValue w tp) where
top = TopV
joinD = joinAbsValue
-- | Join the old and new states and return the updated state iff
-- the result is larger than the old state.
-- This also returns any addresses that are discarded during joining.

26
base/src/Data/Macaw/Analysis/FunctionArgs.hs
View File

@ -46,6 +46,7 @@ import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
import Data.Macaw.CFG
import Data.Macaw.CFG.BlockLabel
import Data.Macaw.CFG.DemandSet
import Data.Macaw.Discovery.State
import Data.Macaw.Fold
import Data.Macaw.Memory
@ -197,6 +198,8 @@ data ArchDemandInfo arch = ArchDemandInfo
, calleeSavedRegs :: !(Set (Some (ArchReg arch)))
-- | Compute the effects of a terminal statement on registers.
, computeArchTermStmtEffects :: !(forall ids . ComputeArchTermStmtEffects arch ids)
-- | Information needed to infer what values are demanded by a AssignRhs and Stmt.
, demandInfoCtx :: !(DemandContext arch)
}
-- | This is information needed to compute dependencies for a single function.
@ -461,17 +464,17 @@ summarizeCall mem lbl proc_state isTailCall = do
recordBlockDemand lbl proc_state (\_ -> DemandAlways) ([Some ip_reg] ++ argRegs)
-- | Return values that must be evaluated to execute side effects.
stmtDemandedValues :: FoldableF (ArchStmt arch)
=> Stmt arch ids
stmtDemandedValues :: DemandContext arch
-> Stmt arch ids
-> [Some (Value arch ids)]
stmtDemandedValues stmt =
stmtDemandedValues ctx stmt = demandConstraints ctx $
case stmt of
-- Assignment statements are side effect free so we ignore them.
AssignStmt a -> case (assignRhs a) of
EvalApp _ -> []
SetUndefined _ -> []
ReadMem addr _ -> [Some addr]
EvalArchFn _ _ -> []
AssignStmt a
| hasSideEffects ctx (assignRhs a) -> do
foldMapFC (\v -> [Some v]) (assignRhs a)
| otherwise ->
[]
WriteMem addr _ v -> [Some addr, Some v]
-- Place holder statements are unknown.
PlaceHolderStmt _ _ -> []
@ -496,9 +499,10 @@ summarizeBlock mem interp_state addr stmts = do
-- Add this label to block demand map with empty set.
blockDemandMap %= Map.insertWith demandMapUnion lbl mempty
ctx <- gets $ demandInfoCtx . archDemandInfo
-- Add all values demanded by non-terminal statements in list.
mapM_ (\(Some v) -> demandValue lbl v)
(concatMap stmtDemandedValues (stmtsNonterm stmts))
mapM_ (mapM_ (\(Some v) -> demandValue lbl v) . stmtDemandedValues ctx)
(stmtsNonterm stmts)
-- Add values demanded by terminal statements
case stmtsTerm stmts of
ParsedTranslateError _ -> do

2
base/src/Data/Macaw/Architecture/Info.hs
View File

@ -124,7 +124,7 @@ data ArchitectureInfo arch
, rewriteArchTermStmt :: (forall s src tgt . ArchTermStmt arch src
-> Rewriter arch s src tgt (ArchTermStmt arch tgt))
-- ^ This rewrites an architecture specific statement
, archDemandContext :: !(forall ids . DemandContext arch ids)
, archDemandContext :: !(DemandContext arch)
-- ^ Provides architecture-specific information for computing which arguments must be
-- evaluated when evaluating a statement.
, postArchTermStmtAbsState :: !(forall ids

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

@ -190,16 +190,6 @@ data App (f :: Type -> *) (tp :: Type) where
----------------------------------------------------------------------
-- Floating point operations
-- | Return true if floating point value is a "quiet" NaN.
FPIsQNaN :: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> App f BoolType
-- | Return true if floating point value is a "signaling" NaN.
FPIsSNaN :: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> App f BoolType
FPAdd :: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> !(f (FloatType flt))
@ -408,8 +398,6 @@ ppAppA pp a0 =
Bsr _ x -> sexprA "bsr" [ pp x ]
-- Floating point
FPIsQNaN rep x -> sexprA "fpIsQNaN" [ prettyPure rep, pp x ]
FPIsSNaN rep x -> sexprA "fpIsSNaN" [ prettyPure rep, pp x ]
FPAdd rep x y -> sexprA "fpAdd" [ prettyPure rep, pp x, pp y ]
FPAddRoundedUp rep x y -> sexprA "fpAddRoundedUp" [ prettyPure rep, pp x, pp y ]
FPSub rep x y -> sexprA "fpSub" [ prettyPure rep, pp x, pp y ]
@ -478,8 +466,6 @@ instance HasRepr (App f) TypeRepr where
Bsr w _ -> BVTypeRepr w
-- Floating point
FPIsQNaN _ _ -> knownType
FPIsSNaN _ _ -> knownType
FPAdd rep _ _ -> floatTypeRepr rep
FPAddRoundedUp{} -> knownType
FPSub rep _ _ -> floatTypeRepr rep

130
base/src/Data/Macaw/CFG/Core.hs
View File

@ -91,6 +91,7 @@ import Control.Monad.State.Strict
import Data.Bits
import Data.Int (Int64)
import Data.Maybe (isNothing, catMaybes)
import Data.Monoid
import Data.Parameterized.Classes
import Data.Parameterized.Map (MapF)
import qualified Data.Parameterized.Map as MapF
@ -106,7 +107,8 @@ import Data.Text (Text)
import qualified Data.Text as Text
import GHC.TypeLits
import Numeric (showHex)
import Text.PrettyPrint.ANSI.Leijen as PP hiding ((<$>))
import Text.PrettyPrint.ANSI.Leijen hiding ((<$>), (<>))
import qualified Text.PrettyPrint.ANSI.Leijen as PP
import Data.Macaw.CFG.App
import Data.Macaw.Memory ( MemWord, MemWidth, MemAddr, MemSegmentOff, Endianness(..)
@ -228,38 +230,7 @@ type ArchMemAddr arch = MemAddr (ArchAddrWidth arch)
type ArchSegmentOff arch = MemSegmentOff (ArchAddrWidth arch)
------------------------------------------------------------------------
-- Value, Assignment, AssignRhs declarations.
-- | A value at runtime.
data Value arch ids tp
= forall n
. (tp ~ BVType n, 1 <= n)
=> BVValue !(NatRepr n) !Integer
-- ^ A constant bitvector
| (tp ~ BoolType)
=> BoolValue !Bool
-- ^ A constant Boolean
| ( tp ~ BVType (ArchAddrWidth arch)
, 1 <= ArchAddrWidth arch
)
=> RelocatableValue !(NatRepr (ArchAddrWidth arch)) !(ArchMemAddr arch)
-- ^ A legal memory address
| AssignedValue !(Assignment arch ids tp)
-- ^ Value from an assignment statement.
| Initial !(ArchReg arch tp)
-- ^ Represents the value assigned to the register when the block started.
type BVValue arch ids w = Value arch ids (BVType w)
-- | A address value for a specific architecture
type ArchAddrValue arch ids = BVValue arch ids (ArchAddrWidth arch)
-- | An assignment consists of a unique location identifier and a right-
-- hand side that returns a value.
data Assignment arch ids tp =
Assignment { assignId :: !(AssignId ids tp)
, assignRhs :: !(AssignRhs arch ids tp)
}
-- MemRepr
-- | The type stored in memory.
--
@ -301,38 +272,94 @@ instance HasRepr MemRepr TypeRepr where
in case leqMulPos (Proxy :: Proxy 8) w of
LeqProof -> BVTypeRepr r
------------------------------------------------------------------------
-- AssignRhs
-- | The right hand side of an assignment is an expression that
-- returns a value.
data AssignRhs (arch :: *) ids tp where
data AssignRhs (arch :: *) (f :: Type -> *) tp where
-- An expression that is computed from evaluating subexpressions.
EvalApp :: !(App (Value arch ids) tp)
-> AssignRhs arch ids tp
EvalApp :: !(App f tp)
-> AssignRhs arch f tp
-- An expression with an undefined value.
SetUndefined :: !(TypeRepr tp)
-> AssignRhs arch ids tp
-> AssignRhs arch f tp
-- Read memory at given location.
ReadMem :: !(ArchAddrValue arch ids)
ReadMem :: !(f (BVType (ArchAddrWidth arch)))
-> !(MemRepr tp)
-> AssignRhs arch ids tp
-> AssignRhs arch f tp
CondReadMem :: !(MemRepr tp)
-> !(f BoolType)
-> !(f (BVType (ArchAddrWidth arch)))
-> !(f tp)
-> AssignRhs arch f tp
-- ^ @CondReadMem tp cond addr v@ reads from memory at the given address if the
-- condition is true and returns the value if it false.
-- Call an architecture specific function that returns some result.
EvalArchFn :: !(ArchFn arch (Value arch ids) tp)
EvalArchFn :: !(ArchFn arch f tp)
-> !(TypeRepr tp)
-> AssignRhs arch ids tp
-> AssignRhs arch f tp
------------------------------------------------------------------------
-- Type operations on assignment AssignRhs, and Value
instance HasRepr (AssignRhs arch ids) TypeRepr where
instance HasRepr (AssignRhs arch f) TypeRepr where
typeRepr rhs =
case rhs of
EvalApp a -> typeRepr a
SetUndefined tp -> tp
ReadMem _ tp -> typeRepr tp
CondReadMem tp _ _ _ -> typeRepr tp
EvalArchFn _ rtp -> rtp
instance FoldableFC (ArchFn arch) => FoldableFC (AssignRhs arch) where
foldMapFC go v =
case v of
EvalApp a -> foldMapFC go a
SetUndefined _w -> mempty
ReadMem addr _ -> go addr
CondReadMem _ c a d -> go c <> go a <> go d
EvalArchFn f _ -> foldMapFC go f
------------------------------------------------------------------------
-- Value and Assignment, AssignRhs declarations.
-- | A value at runtime.
data Value arch ids tp
= forall n
. (tp ~ BVType n, 1 <= n)
=> BVValue !(NatRepr n) !Integer
-- ^ A constant bitvector
| (tp ~ BoolType)
=> BoolValue !Bool
-- ^ A constant Boolean
| ( tp ~ BVType (ArchAddrWidth arch)
, 1 <= ArchAddrWidth arch
)
=> RelocatableValue !(NatRepr (ArchAddrWidth arch)) !(ArchMemAddr arch)
-- ^ A legal memory address
| AssignedValue !(Assignment arch ids tp)
-- ^ Value from an assignment statement.
| Initial !(ArchReg arch tp)
-- ^ Represents the value assigned to the register when the block started.
-- | An assignment consists of a unique location identifier and a right-
-- hand side that returns a value.
data Assignment arch ids tp =
Assignment { assignId :: !(AssignId ids tp)
, assignRhs :: !(AssignRhs arch (Value arch ids) tp)
}
-- | A value with a bitvector type.
type BVValue arch ids w = Value arch ids (BVType w)
-- | A address value for a specific architecture
type ArchAddrValue arch ids = BVValue arch ids (ArchAddrWidth arch)
------------------------------------------------------------------------
-- Type operations on assignment AssignRhs, and Value
instance ( HasRepr (ArchReg arch) TypeRepr
)
=> HasRepr (Value arch ids) TypeRepr where
@ -605,17 +632,19 @@ type ArchConstraints arch
-- | Pretty print an assignment right-hand side using operations parameterized
-- over an application to allow side effects.
ppAssignRhs :: (Applicative m, ArchConstraints arch)
=> (forall u . Value arch ids u -> m Doc)
=> (forall u . f u -> m Doc)
-- ^ Function for pretty printing value.
-> AssignRhs arch ids tp
-> AssignRhs arch f tp
-> m Doc
ppAssignRhs pp (EvalApp a) = ppAppA pp a
ppAssignRhs _ (SetUndefined tp) = pure $ text "undef ::" <+> brackets (text (show tp))
ppAssignRhs pp (ReadMem a repr) =
(\d -> text "read_mem" <+> d <+> PP.parens (pretty repr)) <$> pp a
ppAssignRhs pp (CondReadMem repr c a d) = f <$> pp c <*> pp a <*> pp d
where f cd ad dd = text "read_mem" <+> PP.parens (pretty repr) <+> cd <+> ad <+> dd
ppAssignRhs pp (EvalArchFn f _) = ppArchFn pp f
instance ArchConstraints arch => Pretty (AssignRhs arch ids tp) where
instance ArchConstraints arch => Pretty (AssignRhs arch (Value arch ids) tp) where
pretty = runIdentity . ppAssignRhs (Identity . ppValue 10)
instance ArchConstraints arch => Pretty (Assignment arch ids tp) where
@ -756,11 +785,14 @@ refsInApp :: App (Value arch ids) tp -> Set (Some (AssignId ids))
refsInApp app = foldMapFC refsInValue app
refsInAssignRhs :: FoldableFC (ArchFn arch)
=> AssignRhs arch ids tp
=> AssignRhs arch (Value arch ids) tp
-> Set (Some (AssignId ids))
refsInAssignRhs rhs =
case rhs of
EvalApp v -> refsInApp v
SetUndefined _ -> Set.empty
ReadMem v _ -> refsInValue v
CondReadMem _ c a d ->
Set.union (refsInValue c) $
Set.union (refsInValue a) (refsInValue d)
EvalArchFn f _ -> foldMapFC refsInValue f

39
base/src/Data/Macaw/CFG/DemandSet.hs
View File

@ -3,11 +3,13 @@
{-# LANGUAGE RankNTypes #-}
module Data.Macaw.CFG.DemandSet
( DemandComp
, DemandContext(..)
, AssignIdSet
, runDemandComp
, addValueDemands
, addStmtDemands
-- * DemandContext
, DemandContext(..)
, hasSideEffects
-- * Filtering after demand set is computed.
, stmtNeeded
) where
@ -28,7 +30,7 @@ type AssignIdSet ids = Set (Some (AssignId ids))
-- | This provides the architecture specific functions needed to
-- resolve demand sets.
data DemandContext arch ids
data DemandContext arch
= DemandContext { archFnHasSideEffects :: !(forall v tp . ArchFn arch v tp -> Bool)
-- ^ This returns true if the architecture function has implicit
-- side effects (and thus can be safely removed).
@ -37,17 +39,18 @@ data DemandContext arch ids
=> a) -> a)
}
-- | Return true if assign rhs has side effects (and thus should alwatys be demanded)
hasSideEffects :: DemandContext arch ids -> AssignRhs arch ids tp -> Bool
-- | Return true if assign rhs has side effects (and thus should always be demanded)
hasSideEffects :: DemandContext arch -> AssignRhs arch f tp -> Bool
hasSideEffects ctx rhs =
case rhs of
EvalApp{} -> False
SetUndefined{} -> False
ReadMem{} -> True
CondReadMem{} -> True
EvalArchFn fn _ -> archFnHasSideEffects ctx fn
data DemandState arch ids
= DemandState { demandContext :: !(DemandContext arch ids)
= DemandState { demandContext :: !(DemandContext arch)
, demandedAssignIds :: !(AssignIdSet ids)
}
@ -57,28 +60,12 @@ newtype DemandComp arch ids a = DemandComp { unDemandComp :: State (DemandState
-- | Run demand computation and return the set of assignments that
-- were determined to be needed.
runDemandComp :: DemandContext arch ids -> DemandComp arch ids () -> AssignIdSet ids
runDemandComp :: DemandContext arch -> DemandComp arch ids () -> AssignIdSet ids
runDemandComp ctx comp = demandedAssignIds $ execState (unDemandComp comp) s
where s = DemandState { demandContext = ctx
, demandedAssignIds = Set.empty
}
-- | Record assign ids needed to compute this assignment right-hand
-- side.
addAssignRhsDemands :: AssignRhs arch ids tp -> DemandComp arch ids ()
addAssignRhsDemands rhs =
case rhs of
EvalApp app -> do
traverseFC_ addValueDemands app
SetUndefined{} ->
pure ()
ReadMem addr _ -> do
addValueDemands addr
EvalArchFn fn _ -> do
ctx <- DemandComp $ gets $ demandContext
demandConstraints ctx $
addValueListDemands $ foldMapFC (\v -> [Some v]) fn
-- | Add the ID of this assignment to demand set and also that of any
-- values needed to compute it.
addAssignmentDemands :: Assignment arch ids tp -> DemandComp arch ids ()
@ -88,7 +75,8 @@ addAssignmentDemands a = do
when (Set.notMember thisId (demandedAssignIds s)) $ do
let s' = s { demandedAssignIds = Set.insert thisId (demandedAssignIds s) }
seq s' $ DemandComp $ put s'
addAssignRhsDemands (assignRhs a)
demandConstraints (demandContext s) $
traverseFC_ addValueDemands (assignRhs a)
-- | Add any subassignments needed to compute values to demand set.
addValueDemands :: Value arch ids tp -> DemandComp arch ids ()
@ -100,9 +88,6 @@ addValueDemands v = do
AssignedValue a -> addAssignmentDemands a
Initial{} -> pure ()
addValueListDemands :: [Some (Value arch ids)] -> DemandComp arch ids ()
addValueListDemands = mapM_ (viewSome addValueDemands)
-- | Parse statement, and if it has side effects, add assignments
-- needed to compute statement to demand set.
addStmtDemands :: Stmt arch ids -> DemandComp arch ids ()
@ -124,7 +109,7 @@ addStmtDemands s =
ExecArchStmt astmt -> do
ctx <- DemandComp $ gets $ demandContext
demandConstraints ctx $
addValueListDemands $ foldMapF (\v -> [Some v]) astmt
traverseF_ addValueDemands astmt
------------------------------------------------------------------------
-- Functions for computing demanded values

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

@ -118,7 +118,7 @@ appendRewrittenArchStmt :: ArchStmt arch (Value arch tgt) -> Rewriter arch s src
appendRewrittenArchStmt = appendRewrittenStmt . ExecArchStmt
-- | Add an assignment statement that evaluates the right hand side and return the resulting value.
evalRewrittenRhs :: AssignRhs arch tgt tp -> Rewriter arch s src tgt (Value arch tgt tp)
evalRewrittenRhs :: AssignRhs arch (Value arch tgt) tp -> Rewriter arch s src tgt (Value arch tgt tp)
evalRewrittenRhs rhs = Rewriter $ do
gen <- gets $ rwctxNonceGen . rwContext
aid <- lift $ AssignId <$> freshNonce gen
@ -379,7 +379,8 @@ rewriteApp app = do
_ -> evalRewrittenRhs (EvalApp app)
rewriteAssignRhs :: AssignRhs arch src tp -> Rewriter arch s src tgt (Value arch tgt tp)
rewriteAssignRhs :: AssignRhs arch (Value arch src) tp
-> Rewriter arch s src tgt (Value arch tgt tp)
rewriteAssignRhs rhs =
case rhs of
EvalApp app -> do
@ -388,6 +389,12 @@ rewriteAssignRhs rhs =
ReadMem addr repr -> do
tgtAddr <- rewriteValue addr
evalRewrittenRhs (ReadMem tgtAddr repr)
CondReadMem repr cond addr def -> do
rhs' <- CondReadMem repr
<$> rewriteValue cond
<*> rewriteValue addr
<*> rewriteValue def
evalRewrittenRhs rhs'
EvalArchFn archFn _repr -> do
f <- Rewriter $ gets $ rwctxArchFn . rwContext
f archFn

8
base/src/Data/Macaw/Discovery/AbsEval.hs
View File

@ -42,13 +42,19 @@ absEvalReadMem r a tp
-- | Get the abstract domain for the right-hand side of an assignment.
transferRHS :: ArchitectureInfo a
-> AbsProcessorState (ArchReg a) ids
-> AssignRhs a ids tp
-> AssignRhs a (Value a ids) tp
-> ArchAbsValue a tp
transferRHS info r rhs =
case rhs of
EvalApp app -> withArchConstraints info $ transferApp r app
SetUndefined _ -> TopV
ReadMem a tp -> withArchConstraints info $ absEvalReadMem r a tp
-- TODO: See if we should build a mux specific version
CondReadMem tp _ a d ->
withArchConstraints info $ do
lub (absEvalReadMem r a tp)
(transferValue r d)
EvalArchFn f _ -> absEvalArchFn info r f
-- | Merge in the value of the assignment.

32
base/src/Data/Macaw/Fold.hs
View File

@ -7,9 +7,12 @@ a value without revisiting shared subterms.
-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Macaw.Fold
( Data.Parameterized.TraversableFC.FoldableFC(..)
, foldValueCached
@ -26,25 +29,18 @@ import Data.Macaw.CFG
-- Helper that is a state monad, and also a monoid when the return value
-- is a monoid.
newtype StateMonadMonoid s m = SMM { getStateMonadMonoid :: State s m }
deriving (Functor, Applicative, Monad, MonadState s)
newtype MonadMonoid m a = MM { getMonadMonoid :: m a }
deriving (Functor, Applicative, Monad)
instance MonadState s m => MonadState s (MonadMonoid m) where
get = MM get
put s = MM (put s)
instance Monoid m => Monoid (StateMonadMonoid s m) where
mempty = return mempty
instance (Applicative m, Monoid a) => Monoid (MonadMonoid m a) where
mempty = pure mempty
mappend m m' = mappend <$> m <*> m'
foldAssignRHSValues :: (Monoid r, FoldableFC (ArchFn arch))
=> (forall vtp . Value arch ids vtp -> r)
-> AssignRhs arch ids tp
-> r
foldAssignRHSValues go v =
case v of
EvalApp a -> foldMapFC go a
SetUndefined _w -> mempty
ReadMem addr _ -> go addr
EvalArchFn f _ -> foldMapFC go f
-- | This folds over elements of a values in a values.
--
-- It memoizes values so that it only evaluates assignments with the same id
@ -61,11 +57,11 @@ foldValueCached :: forall m arch ids tp
-- ^ Function for assignments
-> Value arch ids tp
-> State (Map (Some (AssignId ids)) m) m
foldValueCached litf rwf initf assignf = getStateMonadMonoid . go
foldValueCached litf rwf initf assignf = getMonadMonoid . go
where
go :: forall tp'
. Value arch ids tp'
-> StateMonadMonoid (Map (Some (AssignId ids)) m) m
-> MonadMonoid (State (Map (Some (AssignId ids)) m)) m
go v =
case v of
BoolValue b -> return (litf (knownNat :: NatRepr 1) (if b then 1 else 0))
@ -78,6 +74,6 @@ foldValueCached litf rwf initf assignf = getStateMonadMonoid . go
Just v' ->
return $ assignf a_id v'
Nothing -> do
rhs_v <- foldAssignRHSValues go rhs
rhs_v <- foldMapFC go rhs
modify' $ Map.insert (Some a_id) rhs_v
return (assignf a_id rhs_v)

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

@ -8,6 +8,9 @@ module Data.Macaw.TypedList
, Index(..)
, indexValue
, (!)
, index0
, index1
, index2
) where
import Data.Parameterized.Classes
@ -73,3 +76,12 @@ indexValue = go 0
where go :: Integer -> Index l x -> Integer
go i ZeroIndex = i
go i (ConsIndex x) = go (i+1) x
index0 :: Index (x:r) x
index0 = ZeroIndex
index1 :: Index (x0:x1:r) x1
index1 = ConsIndex index0
index2 :: Index (x0:x1:x2:r) x2
index2 = ConsIndex index1

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

@ -147,12 +147,25 @@ instance Show (TypeRepr tp) where
class KnownType tp where
knownType :: TypeRepr tp
class KnownTypeList l where
knownTypeList :: TList TypeRepr l
instance KnownTypeList '[] where
knownTypeList = TList.Empty
instance (KnownType h, KnownTypeList r) => KnownTypeList (h : r) where
knownTypeList = knownType TList.:| knownTypeList
instance KnownType BoolType where
knownType = BoolTypeRepr
instance (KnownNat n, 1 <= n) => KnownType (BVType n) where
knownType = BVTypeRepr knownNat
instance (KnownTypeList l) => KnownType (TupleType l) where
knownType = TupleTypeRepr knownTypeList
------------------------------------------------------------------------
-- Floating point sizes

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

@ -37,7 +37,7 @@ module Data.Macaw.X86
, Data.Macaw.X86.X86Reg.x86FloatResultRegs
, Data.Macaw.X86.X86Reg.x86CalleeSavedRegs
, pattern Data.Macaw.X86.X86Reg.RAX
, x86DemandContext
) where
import Control.Exception (assert)
@ -321,6 +321,7 @@ transferAbsValue r f =
X86IRem{} -> TopV
X86Div{} -> TopV
X86Rem{} -> TopV
UCOMIS{} -> TopV
-- | Disassemble block, returning either an error, or a list of blocks
-- and ending PC.
@ -454,7 +455,7 @@ freeBSD_syscallPersonality =
, spResultRegisters = [ Some RAX ]
}
x86DemandContext :: DemandContext X86_64 ids
x86DemandContext :: DemandContext X86_64
x86DemandContext =
DemandContext { demandConstraints = \a -> a
, archFnHasSideEffects = x86PrimFnHasSideEffects

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

@ -14,6 +14,7 @@ This defines the X86_64 architecture type and the supporting definitions.
module Data.Macaw.X86.ArchTypes
( -- * Architecture
X86_64
, UCOMType(..)
, X86PrimFn(..)
, rewriteX86PrimFn
, x86PrimFnHasSideEffects
@ -173,11 +174,10 @@ data X86PrimFn f tp where
-> !(f (BVType 64))
-> !(f (BVType 64))
-> X86PrimFn f (BVType 64)
-- ^ `RepnzScas sz val base cnt` searchs through a buffer starting at
-- `base` to find an element `i` such that base[i] = val.
-- Each step it increments `i` by 1 and decrements `cnt` by `1`. It returns
-- the final value of `cnt`.
-- Each step it increments `i` by 1 and decrements `cnt` by `1`.
-- It returns the final value of `cnt`, the
MMXExtend :: !(f (BVType 64)) -> X86PrimFn f (BVType 80)
-- ^ This returns a 80-bit value where the high 16-bits are all
-- 1s, and the low 64-bits are the given register.
@ -208,6 +208,35 @@ data X86PrimFn f tp where
-- ^ This performs an unsigned remainder for div.
-- It raises a #DE exception if the divisor is 0 or the quotient overflows.
UCOMIS :: !(UCOMType tp)
-> !(f tp)
-> !(f tp)
-> X86PrimFn f (TupleType [BoolType, BoolType, BoolType])
-- ^ This performs a comparison of two floating point values and returns three flags:
--
-- * ZF is for the zero-flag and true if the arguments are equal or either argument is a NaN.
--
-- * PF records the unordered flag and is true if either value is a NaN.
--
-- * CF is the carry flag, and true if the first floating point argument is less than
-- second or either value is a NaN.
--
-- The order of the flags was chosen to be consistent with the Intel documentation for
-- UCOMISD and UCOMISS.
--
-- The documentation is a bit unclear, but it appears this function implicitly depends
-- on the MXCSR register and may signal if the invalid operation exception #I is
-- not masked or the denomal exception #D if it is not masked.
-- | A single or double value for floating-point restricted to this types.
data UCOMType tp where
UCOMSingle :: UCOMType (FloatType SingleFloat)
UCOMDouble :: UCOMType (FloatType DoubleFloat)
instance HasRepr UCOMType TypeRepr where
typeRepr UCOMSingle = knownType
typeRepr UCOMDouble = knownType
instance HasRepr (X86PrimFn f) TypeRepr where
typeRepr f =
case f of
@ -226,6 +255,7 @@ instance HasRepr (X86PrimFn f) TypeRepr where
X86IRem w _ _ -> typeRepr (repValSizeMemRepr w)
X86Div w _ _ -> typeRepr (repValSizeMemRepr w)
X86Rem w _ _ -> typeRepr (repValSizeMemRepr w)
UCOMIS _ _ _ -> knownType
instance FunctorFC X86PrimFn where
fmapFC = fmapFCDefault
@ -253,6 +283,7 @@ 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
UCOMIS tp x y -> UCOMIS tp <$> go x <*> go y
instance IsArchFn X86PrimFn where
ppArchFn pp f =
@ -274,7 +305,7 @@ instance IsArchFn X86PrimFn where
X86IRem w n d -> sexprA "irem" [ pure (text $ show $ typeWidth $ repValSizeMemRepr w), pp n, pp d ]
X86Div w n d -> sexprA "div" [ pure (text $ show $ typeWidth $ repValSizeMemRepr w), pp n, pp d ]
X86Rem w n d -> sexprA "rem" [ pure (text $ show $ typeWidth $ repValSizeMemRepr w), pp n, pp d ]
UCOMIS _ x y -> sexprA "ucomis" [ pp x, pp y ]
-- | This returns true if evaluating the primitive function implicitly
-- changes the processor state in some way.
@ -296,6 +327,7 @@ x86PrimFnHasSideEffects f =
X86IRem{} -> True -- /\ ..
X86Div{} -> True -- /\ ..
X86Rem{} -> True -- /\ ..
UCOMIS{} -> True
------------------------------------------------------------------------
-- X86Stmt

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

@ -347,7 +347,7 @@ newAssignID = do
gs <- getState
liftM AssignId $ X86G $ lift $ lift $ lift $ freshNonce $ assignIdGen gs
addAssignment :: AssignRhs X86_64 ids tp
addAssignment :: AssignRhs X86_64 (Value X86_64 ids) tp
-> X86Generator st_s ids (Assignment X86_64 ids tp)
addAssignment rhs = do
l <- newAssignID
@ -355,7 +355,7 @@ addAssignment rhs = do
addStmt $ AssignStmt a
pure $! a
evalAssignRhs :: AssignRhs X86_64 ids tp
evalAssignRhs :: AssignRhs X86_64 (Value X86_64 ids) tp
-> X86Generator st_s ids (Expr ids tp)
evalAssignRhs rhs =
ValueExpr . AssignedValue <$> addAssignment rhs

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

@ -29,6 +29,8 @@ module Data.Macaw.X86.Getters
, getAddrRegOrSegment
, getAddrRegSegmentOrImm
, readXMMValue
, readXMMOrMem32
, readXMMOrMem64
-- * Utilities
, reg16Loc
, reg32Loc
@ -385,6 +387,18 @@ getAddrRegSegmentOrImm v =
-- | Get a XMM value
readXMMValue :: F.Value -> X86Generator st ids (Expr ids (BVType 128))
readXMMValue (F.XMMReg r) = get $ fullRegister $ X86_XMMReg r
readXMMValue (F.XMMReg r) = getReg $ X86_XMMReg r
readXMMValue (F.Mem128 a) = readBVAddress a xmmMemRepr
readXMMValue _ = fail "XMM Instruction given unexpected value."
-- | Get the low 32-bits out of an XMM register or a 64-bit XMM address.
readXMMOrMem32 :: F.Value -> X86Generator st ids (Expr ids (BVType 32))
readXMMOrMem32 (F.XMMReg r) = bvTrunc n32 <$> getReg (X86_XMMReg r)
readXMMOrMem32 (F.Mem128 a) = readBVAddress a dwordMemRepr
readXMMOrMem32 _ = fail "XMM Instruction given unexpected value."
-- | Get the low 64-bits out of an XMM register or a 64-bit XMM address.
readXMMOrMem64 :: F.Value -> X86Generator st ids (Expr ids (BVType 64))
readXMMOrMem64 (F.XMMReg r) = bvTrunc n64 <$> getReg (X86_XMMReg r)
readXMMOrMem64 (F.Mem128 a) = readBVAddress a qwordMemRepr
readXMMOrMem64 _ = fail "XMM Instruction given unexpected value."

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

@ -85,9 +85,6 @@ module Data.Macaw.X86.Monad
, (.*)
, (.&&.)
, (.||.)
, isQNaN
, isSNaN
, isAnyNaN
-- * Semantics
, SIMDWidth(..)
, make_undefined
@ -110,7 +107,6 @@ module Data.Macaw.X86.Monad
, memcopy
, memcmp
, memset
, rep_scas
, even_parity
, fnstcw
, getSegmentBase
@ -1661,16 +1657,6 @@ instance IsValue (Expr ids) where
fpFromBV tgt x = app $ FPFromBV x tgt
truncFPToSignedBV tgt src x = app $ TruncFPToSignedBV src x tgt
isQNaN :: FloatInfoRepr flt -> Expr s (FloatType flt) -> Expr s BoolType
isQNaN rep x = app $ FPIsQNaN rep x
isSNaN :: FloatInfoRepr flt -> Expr s (FloatType flt) -> Expr s BoolType
isSNaN rep x = app $ FPIsSNaN rep x
-- | is NaN (quiet and signalling)
isAnyNaN :: FloatInfoRepr flt -> Expr s (FloatType flt) -> Expr s BoolType
isAnyNaN fir v = boolOr (isQNaN fir v) (isSNaN fir v)
(.&&.) :: IsValue v => v BoolType -> v BoolType -> v BoolType
(.&&.) = boolAnd
@ -1955,42 +1941,6 @@ memset count val dest dfl = do
df_v <- eval dfl
addArchStmt $ MemSet count_v val_v dest_v df_v
-- | This will compare a value against the contents of a memory region for equality and/or
-- inequality.
--
-- It accepts the value to compare, a pointer to the start of the region, and
-- the maximum number of elements to compare, which is decremented after each comparison.
-- It returns the value of the count after it has succeeded, or zero if we reached the
-- end without finding a value. A return value of zero is thus ambiguous on whether
-- the value was found in the last iteration, or whether the value was never found.
rep_scas :: Bool
-- ^ Find first matching (True) or not matching (False)
-> Expr ids BoolType
-- ^ Flag indicates direction of search
-- True means we should decrement buffer pointers after each copy.
-- False means we should increment the buffer pointers after each copy.
-> RepValSize w
-- ^ Number of bytes to compare at a time {1, 2, 4, 8}
-> BVExpr ids w
-- ^ Value to compare
-> Addr ids
-- ^ Pointer to first buffer
-> BVExpr ids 64
-- ^ Maximum number of elements to compare
-> X86Generator st ids (BVExpr ids 64)
rep_scas True is_reverse sz val buf count = do
val_v <- eval val
buf_v <- eval buf
count_v <- eval count
is_reverse_v <- eval is_reverse
case is_reverse_v of
BoolValue False ->
evalArchFn (RepnzScas sz val_v buf_v count_v)
_ ->
fail $ "Unsupported rep_scas value " ++ show is_reverse_v
rep_scas False _is_reverse _sz _val _buf _count = do
fail $ "Semantics only currently supports finding elements."
-- | Return true if value contains an even number of true bits.
even_parity :: BVExpr ids 8 -> X86Generator st ids (Expr ids BoolType)
even_parity v = do

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

@ -17,7 +17,6 @@ module Data.Macaw.X86.Semantics
( execInstruction
) where
import Prelude hiding (isNaN)
import Control.Monad (when)
import qualified Data.Bits as Bits
import Data.Foldable
@ -29,11 +28,20 @@ import Data.Parameterized.Some
import Data.Proxy
import qualified Flexdis86 as F
import Data.Macaw.CFG (MemRepr(..), memReprBytes)
import Data.Macaw.CFG ( MemRepr(..)
, memReprBytes
, App(..)
, Value(BoolValue)
, AssignRhs(CondReadMem)
, mkLit
)
import Data.Macaw.Memory (Endianness (LittleEndian))
import Data.Macaw.Types
import qualified Data.Macaw.TypedList as TList
--import qualified Data.Macaw.X86.ArchTypes as X86
import Data.Macaw.X86.ArchTypes
import Data.Macaw.X86.Generator
import Data.Macaw.X86.Getters
import Data.Macaw.X86.InstructionDef
import Data.Macaw.X86.Monad
@ -1147,7 +1155,8 @@ xaxValLoc QWordRepVal = rax
-- The arguments to this are always rax/QWORD PTR es:[rdi], so we only
-- need the args for the size.
exec_scas :: Bool -- Flag indicating if RepZPrefix appeared before instruction
exec_scas :: forall st ids n
. Bool -- Flag indicating if RepZPrefix appeared before instruction
-> Bool -- Flag indicating if RepNZPrefix appeared before instruction
-> RepValSize n
-> X86Generator st ids ()
@ -1163,38 +1172,59 @@ exec_scas False False rep = repValHasSupportedWidth rep $ do
(bvLit n64 (memReprBytes memRepr))
rdi .= v_rdi `bvAdd` bytesPerOp
-- repz or repnz prefix set
exec_scas _repz_pfx repnz_pfx rep = repValHasSupportedWidth rep $ do
let mrepr = repValSizeMemRepr rep
let val_loc = xaxValLoc rep
exec_scas _repz_pfx False _rep =
fail $ "Semantics only currently supports finding elements."
exec_scas _repz_pfx True sz = repValHasSupportedWidth sz $ do
let val_loc = xaxValLoc sz
-- Get the direction flag -- it will be used to determine whether to add or subtract at each step.
-- If the flag is zero, then the register is incremented, otherwise it is incremented.
df <- get df_loc
df <- eval =<< get df_loc
case df of
BoolValue False ->
pure ()
_ ->
fail $ "Unsupported scas value " ++ show df
-- Get value that we are using in comparison
v_rax <- get val_loc
v_rax <- eval =<< get val_loc
-- Get the starting address for the comparsions
v_rdi <- get rdi
v_rdi <- eval =<< get rdi
-- Get maximum number of times to execute instruction
count <- get rcx
unless_ (count .=. bvKLit 0) $ do
v_rcx <- eval =<< get rcx
count' <- evalArchFn (RepnzScas sz v_rax v_rdi v_rcx)
-- Get number of bytes each comparison will use
let bytePerOpLit = bvKLit (memReprBytes (repValSizeMemRepr sz))
count' <- rep_scas repnz_pfx df rep v_rax v_rdi count
-- Count the number of bytes seen.
let nBytesSeen = (ValueExpr v_rcx `bvSub` count') `bvMul` bytePerOpLit
-- Get number of bytes each comparison will use
let bytesPerOp = memReprBytes mrepr
-- Get multiple of each element (negated for direction flag
let bytePerOpLit = mux df (bvKLit (negate bytesPerOp)) (bvKLit bytesPerOp)
let lastWordBytes = nBytesSeen `bvSub` bytePerOpLit
-- Count the number of bytes seen.
let nBytesSeen = (count `bvSub` count') `bvMul` bytePerOpLit
let y = ValueExpr v_rax
let lastWordBytes = nBytesSeen `bvSub` bytePerOpLit
dst <- eval (ValueExpr v_rdi `bvAdd` lastWordBytes)
cond <- eval (ValueExpr v_rcx .=. bvKLit 0)
let condExpr = ValueExpr cond
dst_val <- evalAssignRhs $ CondReadMem (repValSizeMemRepr sz) cond dst (mkLit knownNat 0)
exec_cmp (MemoryAddr (v_rdi `bvAdd` lastWordBytes) mrepr) v_rax
let condSet :: Location (Addr ids) tp -> Expr ids tp -> X86Generator st ids ()
condSet l e = modify l (mux condExpr e)
condSet rcx count'
condSet rdi $ ValueExpr v_rdi `bvAdd` nBytesSeen
condSet of_loc $ ssub_overflows dst_val y
-- Set overflow and arithmetic flags
condSet af_loc $ usub4_overflows dst_val y
condSet cf_loc $ usub_overflows dst_val y
-- Set result value.
let res = dst_val `bvSub` y
condSet sf_loc $ msb res
condSet zf_loc $ is_zero res
byte <- eval (least_byte res)
condSet pf_loc =<< evalArchFn (EvenParity byte)
rdi .= v_rdi `bvAdd` nBytesSeen
rcx .= count'
def_scas :: InstructionDef
def_scas = defBinary "scas" $ \ii loc loc' -> do
@ -1836,33 +1866,47 @@ def_mulps = defBinaryXMMV "mulps" $ \l v -> do
-- SQRTSS Compute square root of scalar single-precision floating-point values
-- 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
-- MAXPS Return maximum packed single-precision floating-point values
-- MAXPS Return maximum packed single-precision floating-poi1nt values
-- MAXSS Return maximum scalar single-precision floating-point values
-- MINPS Return minimum packed single-precision floating-point values
-- MINSS Return minimum scalar single-precision floating-point values
-- *** SSE Comparison Instructions
-- | UCOMISD Perform unordered comparison of scalar double-precision
-- floating-point values and set flags in EFLAGS register.
def_ucomisd :: InstructionDef
-- Invalid (if SNaN operands), Denormal.
def_ucomisd =
defBinary "ucomisd" $ \_ xv yv -> do
x <- eval =<< readXMMOrMem64 xv
y <- eval =<< readXMMOrMem64 yv
res <- evalArchFn (UCOMIS UCOMDouble x y)
zf_loc .= app (TupleField knownTypeList res TList.index0)
pf_loc .= app (TupleField knownTypeList res TList.index1)
cf_loc .= app (TupleField knownTypeList res TList.index2)
of_loc .= false
af_loc .= false
sf_loc .= false
-- CMPPS Compare packed single-precision floating-point values
-- CMPSS Compare scalar single-precision floating-point values
-- COMISS Perform ordered comparison of scalar single-precision floating-point values and set flags in EFLAGS register
-- | UCOMISS Perform unordered comparison of scalar single-precision floating-point values and set flags in EFLAGS register
def_ucomiss :: InstructionDef
-- Invalid (if SNaN operands), Denormal.
def_ucomiss = defBinaryXMMV "ucomiss" $ \l v -> do
v' <- bvTrunc knownNat <$> get l
let fir = SingleFloatRepr
let unordered = (isAnyNaN fir v .||. isAnyNaN fir v')
lt = fpLt fir v' v
eq = fpEq fir v' v
zf_loc .= (unordered .||. eq)
pf_loc .= unordered
cf_loc .= (unordered .||. lt)
of_loc .= false
af_loc .= false
sf_loc .= false
def_ucomiss =
defBinary "ucomiss" $ \_ xv yv -> do
x <- eval =<< readXMMOrMem32 xv
y <- eval =<< readXMMOrMem32 yv
res <- evalArchFn (UCOMIS UCOMSingle x y)
zf_loc .= app (TupleField knownTypeList res TList.index0)
pf_loc .= app (TupleField knownTypeList res TList.index1)
cf_loc .= app (TupleField knownTypeList res TList.index2)
of_loc .= false
af_loc .= false
sf_loc .= false
-- *** SSE Logical Instructions
@ -2176,24 +2220,6 @@ def_cmpsd =
-- COMISD Perform ordered comparison of scalar double-precision floating-point values and set flags in EFLAGS register
-- | UCOMISD Perform unordered comparison of scalar double-precision
-- floating-point values and set flags in EFLAGS register.
def_ucomisd :: InstructionDef
-- Invalid (if SNaN operands), Denormal.
def_ucomisd = defBinaryXMMV "ucomisd" $ \l v -> do
let fir = DoubleFloatRepr
v' <- bvTrunc knownNat <$> get l
let unordered = (isAnyNaN fir v .||. isAnyNaN fir v')
lt = fpLt fir v' v
eq = fpEq fir v' v
zf_loc .= (unordered .||. eq)
pf_loc .= unordered
cf_loc .= (unordered .||. lt)
of_loc .= false
af_loc .= false
sf_loc .= false
-- *** SSE2 Shuffle and Unpack Instructions