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

Separate App/remove ConcatV.

Browse Source
This commit is contained in:
Joe Hendrix 2017-06-02 11:10:58 -07:00
parent 4a145f6b49
commit 51ac2e53a2
No known key found for this signature in database
GPG Key ID: 00F67DE32381DB9F
8 changed files with 676 additions and 753 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
macaw.cabal
View File

@ -32,6 +32,7 @@ library
Data.Macaw.Architecture.Info
Data.Macaw.Architecture.Syscall
Data.Macaw.CFG
Data.Macaw.CFG.App
Data.Macaw.DebugLogging
Data.Macaw.Discovery
Data.Macaw.Discovery.Info

21
src/Data/Macaw/AbsDomain/AbsState.hs
View File

@ -1171,31 +1171,30 @@ transferValue c v =
------------------------------------------------------------------------
-- Operations
addMemWrite :: ( HasRepr (ArchReg arch) TypeRepr
, OrdF (ArchReg arch)
, ShowF (ArchReg arch)
addMemWrite :: ( RegisterInfo (ArchReg arch)
, MemWidth (ArchAddrWidth arch)
)
=> ArchAbsValue arch (BVType (ArchAddrWidth arch))
-- ^ Current instruction pointer
--
-- Used for pretty printing
-> BVValue arch ids (ArchAddrWidth arch)
=> BVValue arch ids (ArchAddrWidth arch)
-- ^ Address that we are writing to.
-> MemRepr tp
-- ^ Information about how value should be represented in memory.
-> Value arch ids tp
-- ^ Value to write to memory
-> AbsProcessorState (ArchReg arch) ids
-- ^ Current processor state.
-> AbsProcessorState (ArchReg arch) ids
addMemWrite cur_ip a memRepr v r =
addMemWrite a memRepr v r =
case (transferValue r a, transferValue r v) of
-- (_,TopV) -> r
-- We overwrite _some_ stack location. An alternative would be to
-- update everything with v.
(SomeStackOffset _, _) ->
(SomeStackOffset _, _) -> do
let cur_ip = r^.absInitialRegs^.curIP
debug DAbsInt ("addMemWrite: dropping stack at "
++ show (pretty cur_ip)
++ " via " ++ show (pretty a)
++" in SomeStackOffset case") $
r & curAbsStack %~ pruneStack
r & curAbsStack %~ pruneStack
(StackOffset _ s, v_abs) ->
let w = valueByteSize v
e = StackEntry memRepr v_abs

40
src/Data/Macaw/Architecture/Info.hs
View File

@ -23,7 +23,6 @@ import Data.Parameterized.Nonce
import Data.Macaw.AbsDomain.AbsState
import Data.Macaw.CFG
import Data.Macaw.Memory
import Data.Macaw.Types
------------------------------------------------------------------------
-- ArchitectureInfo
@ -63,7 +62,10 @@ type DisassembleFn arch
-- | This records architecture specific functions for analysis.
data ArchitectureInfo arch
= ArchitectureInfo
{ archAddrWidth :: !(AddrWidthRepr (RegAddrWidth (ArchReg arch)))
{ withArchConstraints :: forall a . (ArchConstraints arch => a) -> a
-- ^ Provides the architecture constraints to any computation
-- that needs it.
, archAddrWidth :: !(AddrWidthRepr (RegAddrWidth (ArchReg arch)))
-- ^ Architecture address width.
, archEndianness :: !Endianness
-- ^ The byte order values are stored in.
@ -77,9 +79,9 @@ data ArchitectureInfo arch
-- ^ Return true if architecture register should be preserved across a call.
, preserveRegAcrossSyscall :: !(forall tp . ArchReg arch tp -> Bool)
-- ^ Return true if architecture register should be preserved across a system call.
, fnBlockStateFn :: !(Memory (RegAddrWidth (ArchReg arch))
-> SegmentedAddr (RegAddrWidth (ArchReg arch))
-> AbsBlockState (ArchReg arch))
, mkInitialAbsState :: !(Memory (RegAddrWidth (ArchReg arch))
-> SegmentedAddr (RegAddrWidth (ArchReg arch))
-> AbsBlockState (ArchReg arch))
-- ^ Creates an abstract block state for representing the beginning of a
-- function.
, absEvalArchFn :: !(forall ids tp
@ -87,32 +89,32 @@ data ArchitectureInfo arch
-> ArchFn arch ids tp
-> AbsValue (RegAddrWidth (ArchReg arch)) tp)
-- ^ Evaluates an architecture-specific function
, absEvalArchStmt :: !(forall ids
. AbsProcessorState (ArchReg arch) ids
-> ArchStmt arch ids
-> AbsProcessorState (ArchReg arch) ids)
-- ^ Evaluates an architecture-specific statement
}
-- | Return state post call
archPostCallAbsState :: ( RegisterInfo (ArchReg arch)
, HasRepr (ArchReg arch) TypeRepr
)
=> ArchitectureInfo arch
archPostCallAbsState :: ArchitectureInfo arch
-- ^ Architecture information
-> AbsBlockState (ArchReg arch)
-> SegmentedAddr (RegAddrWidth (ArchReg arch))
-> AbsBlockState (ArchReg arch)
archPostCallAbsState archInfo = postCallAbsState params
where params = CallParams { postCallStackDelta = negate (callStackDelta archInfo)
, preserveReg = preserveRegAcrossCall archInfo
}
archPostCallAbsState info = withArchConstraints info $
let params = CallParams { postCallStackDelta = negate (callStackDelta info)
, preserveReg = preserveRegAcrossCall info
}
in postCallAbsState params
-- | Return state post call
archPostSyscallAbsState :: ( RegisterInfo (ArchReg arch)
, HasRepr (ArchReg arch) TypeRepr
)
=> ArchitectureInfo arch
archPostSyscallAbsState :: ArchitectureInfo arch
-- ^ Architecture information
-> AbsBlockState (ArchReg arch)
-> SegmentedAddr (RegAddrWidth (ArchReg arch))
-> AbsBlockState (ArchReg arch)
archPostSyscallAbsState archInfo = postCallAbsState params
archPostSyscallAbsState info = withArchConstraints info $ postCallAbsState params
where params = CallParams { postCallStackDelta = 0
, preserveReg = preserveRegAcrossSyscall archInfo
, preserveReg = preserveRegAcrossSyscall info
}

581
src/Data/Macaw/CFG.hs
View File

@ -4,10 +4,9 @@ Maintainer : Joe Hendrix <jhendrix@galois.com>
Defines data types needed to represent control flow graphs from machine code.
This is a low-level CFG representation where the entire program is a single CFG.
This is a low-level CFG representation where the entire program is a
single CFG.
-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
@ -20,10 +19,8 @@ This is a low-level CFG representation where the entire program is a single CFG.
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Macaw.CFG
( CFG
, emptyCFG
@ -57,14 +54,8 @@ module Data.Macaw.CFG
, bvValue
, ppValueAssignments
, ppValueAssignmentList
, App(..)
-- * App
, appType
, appWidth
, mapApp
, foldApp
, foldAppl
, traverseApp
, module Data.Macaw.CFG.App
-- * RegState
, RegState
, regStateMap
@ -76,13 +67,9 @@ module Data.Macaw.CFG
, traverseRegsWith
, zipWithRegState
-- * Pretty printing
, ppApp
, ppAssignId
, ppLit
, ppNat
, ppValue
, sexpr
, sexprA
, PrettyF(..)
, ArchConstraints(..)
, PrettyRegValue(..)
@ -110,7 +97,6 @@ module Data.Macaw.CFG
, Data.Macaw.Memory.SegmentedAddr
) where
import Control.Applicative
import Control.Exception (assert)
import Control.Lens
import Control.Monad.Identity
@ -128,7 +114,6 @@ import qualified Data.Parameterized.Map as MapF
import Data.Parameterized.NatRepr
import Data.Parameterized.Nonce
import Data.Parameterized.Some
import Data.Parameterized.TH.GADT
import Data.Parameterized.TraversableF
import Data.Set (Set)
import qualified Data.Set as Set
@ -139,6 +124,7 @@ import GHC.TypeLits
import Numeric (showHex)
import Text.PrettyPrint.ANSI.Leijen as PP hiding ((<$>))
import Data.Macaw.CFG.App
import Data.Macaw.Memory (MemWord, MemWidth, SegmentedAddr(..), Endianness)
import Data.Macaw.Types
@ -210,516 +196,14 @@ instance Show (BlockLabel w) where
instance Pretty (BlockLabel w) where
pretty l = text (show l)
-----------------------------------------------------------------------
-- App
-- | App defines builtin operations on values.
data App (f :: Type -> *) (tp :: Type) where
Mux :: !(NatRepr n)
-> !(f BoolType)
-> !(f (BVType n))
-> !(f (BVType n))
-> App f (BVType n)
----------------------------------------------------------------------
-- Operations related to concatenating and extending bitvectors.
-- This returns a 80-bit value where the high 16-bits are all 1s,
-- and the low 64-bits are the given register.
MMXExtend :: !(f (BVType 64))
-> App f (BVType 80)
-- Concatenate two bitvectors together (low-bits are first)
ConcatV :: !(NatRepr n)
-> !(NatRepr m)
-> !(f (BVType n))
-> !(f (BVType m))
-> App f (BVType (n+m))
-- Get upper half of bitvector
UpperHalf :: !(NatRepr n)
-> !(f (BVType (n+n)))
-> App f (BVType n)
-- Truncate a bitvector value.
Trunc :: (1 <= n, n+1 <= m) => !(f (BVType m)) -> !(NatRepr n) -> App f (BVType n)
-- Signed extension.
SExt :: (1 <= m, m+1 <= n) => f (BVType m) -> NatRepr n -> App f (BVType n)
-- Unsigned extension.
UExt :: (1 <= m, m+1 <= n) => f (BVType m) -> NatRepr n -> App f (BVType n)
----------------------------------------------------------------------
-- Boolean operations
AndApp :: !(f BoolType) -> !(f BoolType) -> App f BoolType
OrApp :: !(f BoolType) -> !(f BoolType) -> App f BoolType
NotApp :: !(f BoolType) -> App f BoolType
----------------------------------------------------------------------
-- Bitvector operations
BVAdd :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
BVSub :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
-- Multiply two numbers
BVMul :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
-- Unsigned division (rounds fractions to zero).
--
-- This operation is not defined when the denominator is zero. The
-- caller should raise a #de exception in this case (see
-- 'Reopt.Semantics.Implementation.exec_div').
BVQuot :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
-- Unsigned modulo (rounds fractional results to zero)
--
-- See 'BVQuot' for usage.
BVRem :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
-- Signed division (rounds fractional results to zero).
--
-- See 'BVQuot' for usage.
BVSignedQuot :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
-- Signed modulo (rounds fractional results to zero).
--
-- The resulting modulus has the same sign as the quotient and satisfies
-- the constraint that for all x y where y != 0:
-- x = (y * BVSignedQuot x y) + BVSignedRem x y
--
-- See 'BVQuot' for usage.
BVSignedRem :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
-- Unsigned less than.
BVUnsignedLt :: !(f (BVType n)) -> !(f (BVType n)) -> App f BoolType
-- Unsigned less than or equal.
BVUnsignedLe :: !(f (BVType n)) -> !(f (BVType n)) -> App f BoolType
-- Signed less than
BVSignedLt :: !(f (BVType n)) -> !(f (BVType n)) -> App f BoolType
-- Signed less than or equal.
BVSignedLe :: !(f (BVType n)) -> !(f (BVType n)) -> App f BoolType
-- @BVTestBit x i@ returns true iff bit @i@ of @x@ is true.
-- 0 is the index of the least-significant bit.
BVTestBit :: !(f (BVType n)) -> !(f (BVType log_n)) -> App f BoolType
-- Bitwise complement
BVComplement :: !(NatRepr n) -> !(f (BVType n)) -> App f (BVType n)
-- Bitwise and
BVAnd :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
-- Bitwise or
BVOr :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
-- Exclusive or
BVXor :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
-- Logical left shift (x * 2 ^ n)
BVShl :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
-- Logical right shift (x / 2 ^ n)
BVShr :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
-- Arithmetic right shift (x / 2 ^ n)
BVSar :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
-- Compare for equality.
BVEq :: !(f (BVType n)) -> !(f (BVType n)) -> App f BoolType
-- Return true if value contains even number of true bits.
EvenParity :: !(f (BVType 8)) -> App f BoolType
-- Reverse the bytes in a bitvector expression.
ReverseBytes :: !(NatRepr n) -> !(f (BVType n)) -> App f (BVType n)
-- Add two values and a carry bit to determine if they have an unsigned
-- overflow.
UadcOverflows :: !(NatRepr n)
-> !(f (BVType n))
-> !(f (BVType n))
-> !(f BoolType)
-> App f BoolType
-- Add two values and a carry bit to determine if they have a signed
-- overflow.
SadcOverflows :: !(NatRepr n)
-> !(f (BVType n))
-> !(f (BVType n))
-> !(f BoolType)
-> App f BoolType
-- Unsigned subtract with borrow overflow
UsbbOverflows :: !(NatRepr n)
-> !(f (BVType n))
-> !(f (BVType n))
-> !(f BoolType)
-> App f BoolType
-- Signed subtract with borrow overflow
SsbbOverflows :: !(NatRepr n)
-> !(f (BVType n))
-> !(f (BVType n))
-> !(f BoolType)
-> App f BoolType
-- bsf "bit scan forward" returns the index of the least-significant
-- bit that is 1. Undefined if value is zero.
-- All bits at indices less than return value must be unset.
Bsf :: !(NatRepr n) -> !(f (BVType n)) -> App f (BVType n)
-- bsr "bit scan reverse" returns the index of the most-significant
-- bit that is 1. Undefined if value is zero.
-- All bits at indices greater than return value must be unset.
Bsr :: !(NatRepr n) -> !(f (BVType n)) -> App f (BVType n)
----------------------------------------------------------------------
-- Floating point operations
FPIsQNaN :: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> App f BoolType
FPIsSNaN :: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> App f BoolType
FPAdd :: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> !(f (FloatType flt))
-> App f (FloatType flt)
FPAddRoundedUp :: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> !(f (FloatType flt))
-> App f BoolType
FPSub :: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> !(f (FloatType flt))
-> App f (FloatType flt)
FPSubRoundedUp
:: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> !(f (FloatType flt))
-> App f BoolType
FPMul :: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> !(f (FloatType flt))
-> App f (FloatType flt)
FPMulRoundedUp :: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> !(f (FloatType flt))
-> App f BoolType
-- Divides two floating point numbers.
FPDiv :: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> !(f (FloatType flt))
-> App f (FloatType flt)
-- Compare if one floating is strictly less than another.
FPLt :: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> !(f (FloatType flt))
-> App f BoolType
-- Floating point equality (equates -0 and 0)
FPEq :: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> !(f (FloatType flt))
-> App f BoolType
FPCvt :: !(FloatInfoRepr flt)
-- ^ Input float type
-> !(f (FloatType flt))
-> !(FloatInfoRepr flt')
-- ^ Output float type
-> App f (FloatType flt')
FPCvtRoundsUp :: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> !(FloatInfoRepr flt')
-> App f BoolType
FPFromBV :: !(f (BVType n))
-> !(FloatInfoRepr flt)
-> App f (FloatType flt)
-- Convert a floating point value to a signed integer.
-- If the conversion is inexact, then the value is truncated to zero.
-- If the conversion is out of the range of the bitvector, then a floating
-- point exception should be raised.
-- If that exception is masked, then this returns -1 (as a signed bitvector).
TruncFPToSignedBV :: FloatInfoRepr flt
-> f (FloatType flt)
-> NatRepr n
-> App f (BVType n)
-----------------------------------------------------------------------
-- App utilities
-- Force app to be in template-haskell context.
$(pure [])
instance TestEquality f => Eq (App f tp) where
(==) = \x y -> isJust (testEquality x y)
instance TestEquality f => TestEquality (App f) where
testEquality = $(structuralTypeEquality [t|App|]
[ (DataArg 0 `TypeApp` AnyType, [|testEquality|])
, (ConType [t|NatRepr|] `TypeApp` AnyType, [|testEquality|])
, (ConType [t|FloatInfoRepr|] `TypeApp` AnyType, [|testEquality|])
]
)
instance OrdF f => OrdF (App f) where
compareF = $(structuralTypeOrd [t|App|]
[ (DataArg 0 `TypeApp` AnyType, [|compareF|])
, (ConType [t|NatRepr|] `TypeApp` AnyType, [|compareF|])
, (ConType [t|FloatInfoRepr|] `TypeApp` AnyType, [|compareF|])
]
)
instance OrdF f => Ord (App f tp) where
compare a b = case compareF a b of LTF -> LT
EQF -> EQ
GTF -> GT
traverseApp :: Applicative m
=> (forall u . f u -> m (g u))
-> App f tp
-> m (App g tp)
traverseApp = $(structuralTraversal [t|App|] [])
mapApp :: (forall u . f u -> g u)
-> App f tp
-> App g tp
mapApp f m = runIdentity $ traverseApp (return . f) m
foldApp :: Monoid m => (forall u. f u -> m) -> App f tp -> m
foldApp f m = getConst (traverseApp (\f_u -> Const $ f f_u) m)
newtype FoldFn s a = FoldFn { getFoldFn :: s -> s }
instance Functor (FoldFn s) where
fmap _ (FoldFn g) = FoldFn g
instance Applicative (FoldFn s) where
pure _ = FoldFn id
FoldFn g <*> FoldFn h = FoldFn (\s -> h (g s))
-- | Left-fold over all values in the app
foldAppl :: forall f s tp . (forall u . s -> f u -> s) -> s -> App f tp -> s
foldAppl f s0 a = getFoldFn (traverseApp go a) s0
where go :: f u -> FoldFn s (f u)
go v = FoldFn (\s -> f s v)
------------------------------------------------------------------------
-- App pretty printing
sexpr :: String -> [Doc] -> Doc
sexpr nm d = parens (hsep (text nm : d))
sexprA :: Applicative m => String -> [m Doc] -> m Doc
sexprA nm d = sexpr nm <$> sequenceA d
ppNat :: Applicative m => NatRepr n -> m Doc
ppNat n = pure (text (show n))
prettyPure :: (Applicative m, Pretty v) => v -> m Doc
prettyPure = pure . pretty
ppApp :: (forall u . f u -> Doc)
-> App f tp
-> Doc
ppApp pp a0 = runIdentity $ ppAppA (Identity . pp) a0
ppAppA :: Applicative m
=> (forall u . f u -> m Doc)
-> App f tp
-> m Doc
ppAppA pp a0 =
case a0 of
Mux _ c x y -> sexprA "mux" [ pp c, pp x, pp y ]
MMXExtend e -> sexprA "mmx_extend" [ pp e ]
ConcatV _ _ x y -> sexprA "concat" [ pp x, pp y ]
UpperHalf _ x -> sexprA "upper_half" [ pp x ]
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 ]
AndApp x y -> sexprA "and" [ pp x, pp y ]
OrApp x y -> sexprA "or" [ pp x, pp y ]
NotApp x -> sexprA "not" [ pp x ]
BVAdd _ x y -> sexprA "bv_add" [ pp x, pp y ]
BVSub _ x y -> sexprA "bv_sub" [ pp x, pp y ]
BVMul _ x y -> sexprA "bv_mul" [ pp x, pp y ]
BVQuot _ x y -> sexprA "bv_uquot" [ pp x, pp y ]
BVSignedQuot _ x y -> sexprA "bv_squot" [ pp x, pp y ]
BVRem _ x y -> sexprA "bv_urem" [ pp x, pp y ]
BVSignedRem _ x y -> sexprA "bv_srem" [ pp x, pp y ]
BVUnsignedLt x y -> sexprA "bv_ult" [ pp x, pp y ]
BVUnsignedLe x y -> sexprA "bv_ule" [ pp x, pp y ]
BVSignedLt x y -> sexprA "bv_slt" [ pp x, pp y ]
BVSignedLe x y -> sexprA "bv_sle" [ pp x, pp y ]
BVTestBit x i -> sexprA "bv_testbit" [ pp x, pp i]
BVComplement _ x -> sexprA "bv_complement" [ pp x ]
BVAnd _ x y -> sexprA "bv_and" [ pp x, pp y ]
BVOr _ x y -> sexprA "bv_or" [ pp x, pp y ]
BVXor _ x y -> sexprA "bv_xor" [ pp x, pp y ]
BVShl _ x y -> sexprA "bv_shl" [ pp x, pp y ]
BVShr _ x y -> sexprA "bv_shr" [ pp x, pp y ]
BVSar _ x y -> sexprA "bv_sar" [ pp x, pp y ]
BVEq x y -> sexprA "bv_eq" [ pp x, pp y ]
EvenParity x -> sexprA "even_parity" [ pp x ]
ReverseBytes _ x -> sexprA "reverse_bytes" [ pp x ]
UadcOverflows _ x y c -> sexprA "uadc_overflows" [ pp x, pp y, pp c ]
SadcOverflows _ x y c -> sexprA "sadc_overflows" [ pp x, pp y, pp c ]
UsbbOverflows _ x y c -> sexprA "usbb_overflows" [ pp x, pp y, pp c ]
SsbbOverflows _ x y c -> sexprA "ssbb_overflows" [ pp x, pp y, pp c ]
Bsf _ x -> sexprA "bsf" [ pp x ]
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 ]
FPSubRoundedUp rep x y -> sexprA "fpSubRoundedUp" [ prettyPure rep, pp x, pp y ]
FPMul rep x y -> sexprA "fpMul" [ prettyPure rep, pp x, pp y ]
FPMulRoundedUp rep x y -> sexprA "fpMulRoundedUp" [ prettyPure rep, pp x, pp y ]
FPDiv rep x y -> sexprA "fpDiv" [ prettyPure rep, pp x, pp y ]
FPLt rep x y -> sexprA "fpLt" [ prettyPure rep, pp x, pp y ]
FPEq rep x y -> sexprA "fpEq" [ prettyPure rep, pp x, pp y ]
FPCvt src x tgt -> sexprA "fpCvt" [ prettyPure src, pp x, prettyPure tgt ]
FPCvtRoundsUp src x tgt -> sexprA "fpCvtRoundsUp" [ prettyPure src, pp x, prettyPure tgt ]
FPFromBV x tgt -> sexprA "fpFromBV" [ pp x, prettyPure tgt ]
TruncFPToSignedBV _ x w -> sexprA "truncFP_sbv" [ pp x, ppNat w]
------------------------------------------------------------------------
-- appType
appType :: App f tp -> TypeRepr tp
appType a =
case a of
Mux w _ _ _ -> BVTypeRepr w
MMXExtend{} -> knownType
ConcatV w w' _ _ -> BVTypeRepr (addNat w w')
UpperHalf w _ -> BVTypeRepr w
Trunc _ w -> BVTypeRepr w
SExt _ w -> BVTypeRepr w
UExt _ w -> BVTypeRepr w
AndApp{} -> knownType
OrApp{} -> knownType
NotApp{} -> knownType
BVAdd w _ _ -> BVTypeRepr w
BVSub w _ _ -> BVTypeRepr w
BVMul w _ _ -> BVTypeRepr w
BVQuot w _ _ -> BVTypeRepr w
BVSignedQuot w _ _ -> BVTypeRepr w
BVRem w _ _ -> BVTypeRepr w
BVSignedRem w _ _ -> BVTypeRepr w
BVUnsignedLt{} -> knownType
BVUnsignedLe{} -> knownType
BVSignedLt{} -> knownType
BVSignedLe{} -> knownType
BVTestBit{} -> knownType
BVComplement w _ -> BVTypeRepr w
BVAnd w _ _ -> BVTypeRepr w
BVOr w _ _ -> BVTypeRepr w
BVXor w _ _ -> BVTypeRepr w
BVShl w _ _ -> BVTypeRepr w
BVShr w _ _ -> BVTypeRepr w
BVSar w _ _ -> BVTypeRepr w
BVEq _ _ -> knownType
EvenParity _ -> knownType
ReverseBytes w _ -> BVTypeRepr w
UadcOverflows{} -> knownType
SadcOverflows{} -> knownType
UsbbOverflows{} -> knownType
SsbbOverflows{} -> knownType
Bsf w _ -> BVTypeRepr w
Bsr w _ -> BVTypeRepr w
-- Floating point
FPIsQNaN _ _ -> knownType
FPIsSNaN _ _ -> knownType
FPAdd rep _ _ -> floatTypeRepr rep
FPAddRoundedUp{} -> knownType
FPSub rep _ _ -> floatTypeRepr rep
FPSubRoundedUp{} -> knownType
FPMul rep _ _ -> floatTypeRepr rep
FPMulRoundedUp{} -> knownType
FPDiv rep _ _ -> floatTypeRepr rep
FPLt{} -> knownType
FPEq{} -> knownType
FPCvt _ _ tgt -> floatTypeRepr tgt
FPCvtRoundsUp{} -> knownType
FPFromBV _ tgt -> floatTypeRepr tgt
TruncFPToSignedBV _ _ w -> BVTypeRepr w
appWidth :: App f (BVType n) -> NatRepr n
appWidth a =
case appType a of
BVTypeRepr n -> n
$(pure [])
------------------------------------------------------------------------
-- Type families for architecture specific components.
-- | Width of register used to store addresses.
type family RegAddrWidth (r :: Type -> *) :: Nat
-- | The value used to store
type RegAddr r = MemWord (RegAddrWidth r)
-- | A type family for architecture specific functions.
--
-- These function may return a value. They may depend on the current state of
-- the heap, but should not affect the processor state.
--
-- The function may depend on the set of registers defined so far, and the type
-- of the result.
type family ArchFn (arch :: *) :: * -> Type -> *
-- | A type family for defining architecture specific registers that are
-- assigned as part of the language.
type family ArchReg (arch :: *) :: Type -> *
-- | A type family for defining architecture-specific statements that are
-- part of the language.
type family ArchStmt (arch :: *) :: * -> *
-- | The type to use for addresses on the architecutre.
type ArchAddr arch = RegAddr (ArchReg arch)
-- | Number of bits in addreses for architecture.
type ArchAddrWidth arch = RegAddrWidth (ArchReg arch)
-- | A segmented addr for a given architecture.
type ArchSegmentedAddr arch = SegmentedAddr (ArchAddrWidth arch)
type ArchLabel arch = BlockLabel (ArchAddrWidth arch)
------------------------------------------------------------------------
-- AssignId
-- | An 'AssignId' is a unique identifier used to identify assignment
-- statements, in a manner similar to SSA (single static assignment)
-- form. 'AssignId's are typed, and also include a type variable @ids@ that
-- intuitively denotes the set of identifiers from which they are drawn.
-- form. 'AssignId's are typed, and also include a type variable @ids@
-- that intuitively denotes the set of identifiers from which they are
-- drawn.
newtype AssignId (ids :: *) (tp :: Type) = AssignId (Nonce ids tp)
ppAssignId :: AssignId ids tp -> Doc
@ -737,6 +221,49 @@ instance ShowF (AssignId ids) where
instance Show (AssignId ids tp) where
show (AssignId n) = show n
------------------------------------------------------------------------
-- Type families for architecture specific components.
-- | Width of register used to store addresses.
type family RegAddrWidth (r :: Type -> *) :: Nat
-- | The value used to store
type RegAddr r = MemWord (RegAddrWidth r)
-- | Type family for defining what a "register" is for this architecture.
--
-- Registers include things like the general purpose registers, any flag
-- registers that can be read and written without side effects,
type family ArchReg (arch :: *) :: Type -> *
-- | A type family for architecture specific functions.
--
-- These function may return a value. They may depend on the current state of
-- the heap, but should not affect the processor state.
--
-- The function may depend on the set of registers defined so far, and the type
-- of the result.
type family ArchFn (arch :: *) :: * -> Type -> *
-- | A type family for defining architecture-specific statements.
--
-- The second type parameter is the ids phantom type used to provide
-- uniqueness of Nonce values that identify assignments.
--
type family ArchStmt (arch :: *) :: * -> *
-- | The type to use for addresses on the architecutre.
type ArchAddr arch = RegAddr (ArchReg arch)
-- | Number of bits in addreses for architecture.
type ArchAddrWidth arch = RegAddrWidth (ArchReg arch)
-- | A segmented addr for a given architecture.
type ArchSegmentedAddr arch = SegmentedAddr (ArchAddrWidth arch)
type ArchLabel arch = BlockLabel (ArchAddrWidth arch)
------------------------------------------------------------------------
-- Value, Assignment, AssignRhs declarations.
@ -817,7 +344,7 @@ data AssignRhs (arch :: *) ids tp where
instance HasRepr (AssignRhs arch ids) TypeRepr where
typeRepr rhs =
case rhs of
EvalApp a -> appType a
EvalApp a -> typeRepr a
SetUndefined w -> BVTypeRepr w
ReadMem _ tp -> typeRepr tp
EvalArchFn _ rtp -> rtp
@ -838,8 +365,6 @@ valueWidth v =
case typeRepr v of
BVTypeRepr n -> n
$(pure [])
------------------------------------------------------------------------
-- Value equality
@ -1080,8 +605,6 @@ instance ArchConstraints arch => Pretty (AssignRhs arch ids tp) where
instance ArchConstraints arch => Pretty (Assignment arch ids tp) where
pretty (Assignment lhs rhs) = ppAssignId lhs <+> text ":=" <+> pretty rhs
$(pure [])
------------------------------------------------------------------------
-- Pretty print a value assignment
@ -1132,8 +655,6 @@ ppValueAssignmentList vals =
docs <- mapM (collectValueRep 0) vals
return $ brackets $ hcat (punctuate comma docs)
$(pure [])
------------------------------------------------------------------------
-- Pretty printing RegState

492
src/Data/Macaw/CFG/App.hs Normal file
View File

@ -0,0 +1,492 @@
{-|
Copyright : (c) Galois, Inc 2015-2017
Maintainer : Joe Hendrix <jhendrix@galois.com>
This defines a data type `App` for representing operations that can be
applied to a range of values. We call it an `App` because it
represents an application of an operation. In mathematics, we would
probably call it a signature.
-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}
module Data.Macaw.CFG.App
( -- * Constructor
App(..)
-- * Traversals
, mapApp
, foldApp
, foldAppl
, traverseApp
-- * Folding
, ppApp
, ppAppA
-- * Utilities
, ppNat
, sexpr
, sexprA
) where
import Control.Applicative
import Control.Monad.Identity
import Data.Parameterized.Classes
import Data.Parameterized.NatRepr
import Data.Parameterized.TH.GADT
import Text.PrettyPrint.ANSI.Leijen as PP hiding ((<$>))
import Data.Macaw.Types
-----------------------------------------------------------------------
-- App
-- | App defines builtin operations on values.
data App (f :: Type -> *) (tp :: Type) where
Mux :: !(NatRepr n)
-> !(f BoolType)
-> !(f (BVType n))
-> !(f (BVType n))
-> App f (BVType n)
----------------------------------------------------------------------
-- Operations related to concatenating and extending bitvectors.
-- This returns a 80-bit value where the high 16-bits are all 1s,
-- and the low 64-bits are the given register.
MMXExtend :: !(f (BVType 64))
-> App f (BVType 80)
-- Get upper half of bitvector
UpperHalf :: !(NatRepr n)
-> !(f (BVType (n+n)))
-> App f (BVType n)
-- Truncate a bitvector value.
Trunc :: (1 <= n, n+1 <= m) => !(f (BVType m)) -> !(NatRepr n) -> App f (BVType n)
-- Signed extension.
SExt :: (1 <= m, m+1 <= n) => f (BVType m) -> NatRepr n -> App f (BVType n)
-- Unsigned extension.
UExt :: (1 <= m, m+1 <= n) => f (BVType m) -> NatRepr n -> App f (BVType n)
----------------------------------------------------------------------
-- Boolean operations
AndApp :: !(f BoolType) -> !(f BoolType) -> App f BoolType
OrApp :: !(f BoolType) -> !(f BoolType) -> App f BoolType
NotApp :: !(f BoolType) -> App f BoolType
----------------------------------------------------------------------
-- Bitvector operations
BVAdd :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
BVSub :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
-- Multiply two numbers
BVMul :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
-- Unsigned division (rounds fractions to zero).
--
-- This operation is not defined when the denominator is zero. The
-- caller should raise a #de exception in this case (see
-- 'Reopt.Semantics.Implementation.exec_div').
BVQuot :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
-- Unsigned modulo (rounds fractional results to zero)
--
-- See 'BVQuot' for usage.
BVRem :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
-- Signed division (rounds fractional results to zero).
--
-- See 'BVQuot' for usage.
BVSignedQuot :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
-- Signed modulo (rounds fractional results to zero).
--
-- The resulting modulus has the same sign as the quotient and satisfies
-- the constraint that for all x y where y != 0:
-- x = (y * BVSignedQuot x y) + BVSignedRem x y
--
-- See 'BVQuot' for usage.
BVSignedRem :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
-- Unsigned less than.
BVUnsignedLt :: !(f (BVType n)) -> !(f (BVType n)) -> App f BoolType
-- Unsigned less than or equal.
BVUnsignedLe :: !(f (BVType n)) -> !(f (BVType n)) -> App f BoolType
-- Signed less than
BVSignedLt :: !(f (BVType n)) -> !(f (BVType n)) -> App f BoolType
-- Signed less than or equal.
BVSignedLe :: !(f (BVType n)) -> !(f (BVType n)) -> App f BoolType
-- @BVTestBit x i@ returns true iff bit @i@ of @x@ is true.
-- 0 is the index of the least-significant bit.
BVTestBit :: !(f (BVType n)) -> !(f (BVType log_n)) -> App f BoolType
-- Bitwise complement
BVComplement :: !(NatRepr n) -> !(f (BVType n)) -> App f (BVType n)
-- Bitwise and
BVAnd :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
-- Bitwise or
BVOr :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
-- Exclusive or
BVXor :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
-- Logical left shift (x * 2 ^ n)
BVShl :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
-- Logical right shift (x / 2 ^ n)
BVShr :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
-- Arithmetic right shift (x / 2 ^ n)
BVSar :: !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
-- Compare for equality.
BVEq :: !(f (BVType n)) -> !(f (BVType n)) -> App f BoolType
-- Return true if value contains even number of true bits.
EvenParity :: !(f (BVType 8)) -> App f BoolType
-- Reverse the bytes in a bitvector expression.
ReverseBytes :: !(NatRepr n) -> !(f (BVType n)) -> App f (BVType n)
-- Add two values and a carry bit to determine if they have an unsigned
-- overflow.
UadcOverflows :: !(NatRepr n)
-> !(f (BVType n))
-> !(f (BVType n))
-> !(f BoolType)
-> App f BoolType
-- Add two values and a carry bit to determine if they have a signed
-- overflow.
SadcOverflows :: !(NatRepr n)
-> !(f (BVType n))
-> !(f (BVType n))
-> !(f BoolType)
-> App f BoolType
-- Unsigned subtract with borrow overflow
UsbbOverflows :: !(NatRepr n)
-> !(f (BVType n))
-> !(f (BVType n))
-> !(f BoolType)
-> App f BoolType
-- Signed subtract with borrow overflow
SsbbOverflows :: !(NatRepr n)
-> !(f (BVType n))
-> !(f (BVType n))
-> !(f BoolType)
-> App f BoolType
-- bsf "bit scan forward" returns the index of the least-significant
-- bit that is 1. Undefined if value is zero.
-- All bits at indices less than return value must be unset.
Bsf :: !(NatRepr n) -> !(f (BVType n)) -> App f (BVType n)
-- bsr "bit scan reverse" returns the index of the most-significant
-- bit that is 1. Undefined if value is zero.
-- All bits at indices greater than return value must be unset.
Bsr :: !(NatRepr n) -> !(f (BVType n)) -> App f (BVType n)
----------------------------------------------------------------------
-- Floating point operations
FPIsQNaN :: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> App f BoolType
FPIsSNaN :: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> App f BoolType
FPAdd :: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> !(f (FloatType flt))
-> App f (FloatType flt)
FPAddRoundedUp :: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> !(f (FloatType flt))
-> App f BoolType
FPSub :: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> !(f (FloatType flt))
-> App f (FloatType flt)
FPSubRoundedUp
:: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> !(f (FloatType flt))
-> App f BoolType
FPMul :: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> !(f (FloatType flt))
-> App f (FloatType flt)
FPMulRoundedUp :: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> !(f (FloatType flt))
-> App f BoolType
-- Divides two floating point numbers.
FPDiv :: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> !(f (FloatType flt))
-> App f (FloatType flt)
-- Compare if one floating is strictly less than another.
FPLt :: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> !(f (FloatType flt))
-> App f BoolType
-- Floating point equality (equates -0 and 0)
FPEq :: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> !(f (FloatType flt))
-> App f BoolType
FPCvt :: !(FloatInfoRepr flt)
-- ^ Input float type
-> !(f (FloatType flt))
-> !(FloatInfoRepr flt')
-- ^ Output float type
-> App f (FloatType flt')
FPCvtRoundsUp :: !(FloatInfoRepr flt)
-> !(f (FloatType flt))
-> !(FloatInfoRepr flt')
-> App f BoolType
FPFromBV :: !(f (BVType n))
-> !(FloatInfoRepr flt)
-> App f (FloatType flt)
-- Convert a floating point value to a signed integer.
-- If the conversion is inexact, then the value is truncated to zero.
-- If the conversion is out of the range of the bitvector, then a floating
-- point exception should be raised.
-- If that exception is masked, then this returns -1 (as a signed bitvector).
TruncFPToSignedBV :: FloatInfoRepr flt
-> f (FloatType flt)
-> NatRepr n
-> App f (BVType n)
-----------------------------------------------------------------------
-- App utilities
-- Force app to be in template-haskell context.
$(pure [])
instance TestEquality f => Eq (App f tp) where
(==) = \x y -> isJust (testEquality x y)
instance TestEquality f => TestEquality (App f) where
testEquality = $(structuralTypeEquality [t|App|]
[ (DataArg 0 `TypeApp` AnyType, [|testEquality|])
, (ConType [t|NatRepr|] `TypeApp` AnyType, [|testEquality|])
, (ConType [t|FloatInfoRepr|] `TypeApp` AnyType, [|testEquality|])
]
)
instance OrdF f => OrdF (App f) where
compareF = $(structuralTypeOrd [t|App|]
[ (DataArg 0 `TypeApp` AnyType, [|compareF|])
, (ConType [t|NatRepr|] `TypeApp` AnyType, [|compareF|])
, (ConType [t|FloatInfoRepr|] `TypeApp` AnyType, [|compareF|])
]
)
instance OrdF f => Ord (App f tp) where
compare a b = case compareF a b of LTF -> LT
EQF -> EQ
GTF -> GT
traverseApp :: Applicative m
=> (forall u . f u -> m (g u))
-> App f tp
-> m (App g tp)
traverseApp = $(structuralTraversal [t|App|] [])
mapApp :: (forall u . f u -> g u)
-> App f tp
-> App g tp
mapApp f m = runIdentity $ traverseApp (return . f) m
foldApp :: Monoid m => (forall u. f u -> m) -> App f tp -> m
foldApp f m = getConst (traverseApp (\f_u -> Const $ f f_u) m)
newtype FoldFn s a = FoldFn { getFoldFn :: s -> s }
instance Functor (FoldFn s) where
fmap _ (FoldFn g) = FoldFn g
instance Applicative (FoldFn s) where
pure _ = FoldFn id
FoldFn g <*> FoldFn h = FoldFn (\s -> h (g s))
-- | Left-fold over all values in the app
foldAppl :: forall (f :: Type -> *) s tp . (forall u . s -> f u -> s) -> s -> App f tp -> s
foldAppl f s0 a = getFoldFn (traverseApp go a) s0
where go :: f u -> FoldFn s (f u)
go v = FoldFn (\s -> f s v)
------------------------------------------------------------------------
-- App pretty printing
sexpr :: String -> [Doc] -> Doc
sexpr nm d = parens (hsep (text nm : d))
sexprA :: Applicative m => String -> [m Doc] -> m Doc
sexprA nm d = sexpr nm <$> sequenceA d
ppNat :: Applicative m => NatRepr n -> m Doc
ppNat n = pure (text (show n))
prettyPure :: (Applicative m, Pretty v) => v -> m Doc
prettyPure = pure . pretty
ppApp :: (forall u . f u -> Doc)
-> App f tp
-> Doc
ppApp pp a0 = runIdentity $ ppAppA (Identity . pp) a0
ppAppA :: Applicative m
=> (forall u . f u -> m Doc)
-> App f tp
-> m Doc
ppAppA pp a0 =
case a0 of
Mux _ c x y -> sexprA "mux" [ pp c, pp x, pp y ]
MMXExtend e -> sexprA "mmx_extend" [ pp e ]
UpperHalf _ x -> sexprA "upper_half" [ pp x ]
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 ]
AndApp x y -> sexprA "and" [ pp x, pp y ]
OrApp x y -> sexprA "or" [ pp x, pp y ]
NotApp x -> sexprA "not" [ pp x ]
BVAdd _ x y -> sexprA "bv_add" [ pp x, pp y ]
BVSub _ x y -> sexprA "bv_sub" [ pp x, pp y ]
BVMul _ x y -> sexprA "bv_mul" [ pp x, pp y ]
BVQuot _ x y -> sexprA "bv_uquot" [ pp x, pp y ]
BVSignedQuot _ x y -> sexprA "bv_squot" [ pp x, pp y ]
BVRem _ x y -> sexprA "bv_urem" [ pp x, pp y ]
BVSignedRem _ x y -> sexprA "bv_srem" [ pp x, pp y ]
BVUnsignedLt x y -> sexprA "bv_ult" [ pp x, pp y ]
BVUnsignedLe x y -> sexprA "bv_ule" [ pp x, pp y ]
BVSignedLt x y -> sexprA "bv_slt" [ pp x, pp y ]
BVSignedLe x y -> sexprA "bv_sle" [ pp x, pp y ]
BVTestBit x i -> sexprA "bv_testbit" [ pp x, pp i]
BVComplement _ x -> sexprA "bv_complement" [ pp x ]
BVAnd _ x y -> sexprA "bv_and" [ pp x, pp y ]
BVOr _ x y -> sexprA "bv_or" [ pp x, pp y ]
BVXor _ x y -> sexprA "bv_xor" [ pp x, pp y ]
BVShl _ x y -> sexprA "bv_shl" [ pp x, pp y ]
BVShr _ x y -> sexprA "bv_shr" [ pp x, pp y ]
BVSar _ x y -> sexprA "bv_sar" [ pp x, pp y ]
BVEq x y -> sexprA "bv_eq" [ pp x, pp y ]
EvenParity x -> sexprA "even_parity" [ pp x ]
ReverseBytes _ x -> sexprA "reverse_bytes" [ pp x ]
UadcOverflows _ x y c -> sexprA "uadc_overflows" [ pp x, pp y, pp c ]
SadcOverflows _ x y c -> sexprA "sadc_overflows" [ pp x, pp y, pp c ]
UsbbOverflows _ x y c -> sexprA "usbb_overflows" [ pp x, pp y, pp c ]
SsbbOverflows _ x y c -> sexprA "ssbb_overflows" [ pp x, pp y, pp c ]
Bsf _ x -> sexprA "bsf" [ pp x ]
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 ]
FPSubRoundedUp rep x y -> sexprA "fpSubRoundedUp" [ prettyPure rep, pp x, pp y ]
FPMul rep x y -> sexprA "fpMul" [ prettyPure rep, pp x, pp y ]
FPMulRoundedUp rep x y -> sexprA "fpMulRoundedUp" [ prettyPure rep, pp x, pp y ]
FPDiv rep x y -> sexprA "fpDiv" [ prettyPure rep, pp x, pp y ]
FPLt rep x y -> sexprA "fpLt" [ prettyPure rep, pp x, pp y ]
FPEq rep x y -> sexprA "fpEq" [ prettyPure rep, pp x, pp y ]
FPCvt src x tgt -> sexprA "fpCvt" [ prettyPure src, pp x, prettyPure tgt ]
FPCvtRoundsUp src x tgt -> sexprA "fpCvtRoundsUp" [ prettyPure src, pp x, prettyPure tgt ]
FPFromBV x tgt -> sexprA "fpFromBV" [ pp x, prettyPure tgt ]
TruncFPToSignedBV _ x w -> sexprA "truncFP_sbv" [ pp x, ppNat w]
------------------------------------------------------------------------
-- appType
instance HasRepr (App f) TypeRepr where
typeRepr a =
case a of
Mux w _ _ _ -> BVTypeRepr w
MMXExtend{} -> knownType
UpperHalf w _ -> BVTypeRepr w
Trunc _ w -> BVTypeRepr w
SExt _ w -> BVTypeRepr w
UExt _ w -> BVTypeRepr w
AndApp{} -> knownType
OrApp{} -> knownType
NotApp{} -> knownType
BVAdd w _ _ -> BVTypeRepr w
BVSub w _ _ -> BVTypeRepr w
BVMul w _ _ -> BVTypeRepr w
BVQuot w _ _ -> BVTypeRepr w
BVSignedQuot w _ _ -> BVTypeRepr w
BVRem w _ _ -> BVTypeRepr w
BVSignedRem w _ _ -> BVTypeRepr w
BVUnsignedLt{} -> knownType
BVUnsignedLe{} -> knownType
BVSignedLt{} -> knownType
BVSignedLe{} -> knownType
BVTestBit{} -> knownType
BVComplement w _ -> BVTypeRepr w
BVAnd w _ _ -> BVTypeRepr w
BVOr w _ _ -> BVTypeRepr w
BVXor w _ _ -> BVTypeRepr w
BVShl w _ _ -> BVTypeRepr w
BVShr w _ _ -> BVTypeRepr w
BVSar w _ _ -> BVTypeRepr w
BVEq _ _ -> knownType
EvenParity _ -> knownType
ReverseBytes w _ -> BVTypeRepr w
UadcOverflows{} -> knownType
SadcOverflows{} -> knownType
UsbbOverflows{} -> knownType
SsbbOverflows{} -> knownType
Bsf w _ -> BVTypeRepr w
Bsr w _ -> BVTypeRepr w
-- Floating point
FPIsQNaN _ _ -> knownType
FPIsSNaN _ _ -> knownType
FPAdd rep _ _ -> floatTypeRepr rep
FPAddRoundedUp{} -> knownType
FPSub rep _ _ -> floatTypeRepr rep
FPSubRoundedUp{} -> knownType
FPMul rep _ _ -> floatTypeRepr rep
FPMulRoundedUp{} -> knownType
FPDiv rep _ _ -> floatTypeRepr rep
FPLt{} -> knownType
FPEq{} -> knownType
FPCvt _ _ tgt -> floatTypeRepr tgt
FPCvtRoundsUp{} -> knownType
FPFromBV _ tgt -> floatTypeRepr tgt
TruncFPToSignedBV _ _ w -> BVTypeRepr w

272
src/Data/Macaw/Discovery.hs
View File

@ -22,7 +22,6 @@ interleaved abstract interpretation.
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Data.Macaw.Discovery
( cfgFromAddrs
, assignmentAbsValues
@ -50,7 +49,6 @@ import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.Vector as V
import Data.Word
import Numeric
import Debug.Trace
@ -81,36 +79,27 @@ transferReadMem r a tp
| otherwise = TopV
-- | Get the abstract domain for the right-hand side of an assignment.
transferRHS :: forall a ids tp
. ( OrdF (ArchReg a)
, ShowF (ArchReg a)
, MemWidth (ArchAddrWidth a)
)
=> ArchitectureInfo a
transferRHS :: ArchitectureInfo a
-> AbsProcessorState (ArchReg a) ids
-> AssignRhs a ids tp
-> ArchAbsValue a tp
transferRHS info r rhs =
case rhs of
EvalApp app -> transferApp r app
EvalApp app -> withArchConstraints info $ transferApp r app
SetUndefined _ -> TopV
ReadMem a tp -> transferReadMem r a tp
ReadMem a tp -> withArchConstraints info $ transferReadMem r a tp
EvalArchFn f _ -> absEvalArchFn info r f
-- | Merge in the value of the assignment.
--
-- If we have already seen a value, this will combine with meet.
addAssignment :: ( OrdF (ArchReg a)
, ShowF (ArchReg a)
, MemWidth (ArchAddrWidth a)
)
=> ArchitectureInfo a
addAssignment :: ArchitectureInfo a
-> Assignment a ids tp
-> AbsProcessorState (ArchReg a) ids
-> AbsProcessorState (ArchReg a) ids
addAssignment info a c =
addAssignment info a c = withArchConstraints info $
c & (absAssignments . assignLens (assignId a))
%~ flip meet (transferRHS info c (assignRhs a))
%~ (`meet` transferRHS info c (assignRhs a))
------------------------------------------------------------------------
-- Utilities
@ -183,6 +172,7 @@ cameFromUnsoundReason found_map rsn = do
------------------------------------------------------------------------
-- Memory utilities
-- | Return true if range is entirely contained within a single read only segment.Q
rangeInReadonlySegment :: MemWidth w
=> SegmentedAddr w -- ^ Start of range
@ -222,9 +212,24 @@ runCFGM arch_info mem symbols m = do
let init_info = emptyDiscoveryInfo nonce_gen mem symbols arch_info
Some <$> execStateT (unCFGM m) init_info
------------------------------------------------------------------------
-- FunM
liftST :: ST ids a -> CFGM arch ids a
liftST = CFGM . lift
-- | Mark a escaped code pointer as a function entry.
markAddrAsFunction :: CodeAddrReason (ArchAddrWidth arch)
-> ArchSegmentedAddr arch
-> CFGM arch ids ()
markAddrAsFunction rsn addr = do
s <- get
when (not (Set.member addr (s^.functionEntries))) $ do
let _high = Set.lookupGT addr (s^.functionEntries)
modify $ (functionEntries %~ Set.insert addr)
. (function_frontier %~ Map.insert addr rsn)
------------------------------------------------------------------------
-- FunState
-- | The state for the function explroation monad
data FunState arch ids
= FunState { curFunAddr :: !(ArchSegmentedAddr arch)
, _curFunInfo :: !(DiscoveryFunInfo arch ids)
@ -244,6 +249,9 @@ curFunInfo = lens _curFunInfo (\s v -> s { _curFunInfo = v })
frontier :: Simple Lens (FunState arch ids) (Set (ArchSegmentedAddr arch))
frontier = lens _frontier (\s v -> s { _frontier = v })
------------------------------------------------------------------------
-- FunM
-- | A newtype around a function
newtype FunM arch ids a = FunM { unFunM :: StateT (FunState arch ids) (CFGM arch ids) a }
deriving (Functor, Applicative, Monad)
@ -255,136 +263,36 @@ instance MonadState (FunState arch ids) (FunM arch ids) where
liftCFG :: CFGM arch ids a -> FunM arch ids a
liftCFG m = FunM (lift m)
liftST :: ST ids a -> CFGM arch ids a
liftST = CFGM . lift
------------------------------------------------------------------------
-- Block discovery
{-
-- | This is the worker for getBlock, in the case that we have not already
-- read the block.
tryDisassembleAddr :: ArchConstraints arch
=> ArchSegmentedAddr arch
-- ^ Address to disassemble
-> AbsBlockState (ArchReg arch)
-- ^ Abstract state at beginning of block
-> CFGM arch ids ()
tryDisassembleAddr addr ab = do
s0 <- get
-- Attempt to disassemble block.
-- Get memory so that we can decode from it.
let block_addrs = s0^.blocks
-- Returns true if we are not at the start of a block.
-- This is used to stop the disassembler when we reach code
-- that is part of a new block.
let not_at_block = (`Map.notMember` block_addrs)
let mem = memory s0
let nonce_gen = nonceGen s0
(bs, next_ip, maybeError) <- liftST $ disassembleFn (archInfo s0) nonce_gen mem not_at_block addr ab
-- Build state for exploring this.
case maybeError of
Just e -> do
trace ("Failed to disassemble " ++ show e) $ pure ()
Nothing -> do
pure ()
assert (segmentIndex (addrSegment next_ip) == segmentIndex (addrSegment addr)) $ do
assert (next_ip^.addrOffset > addr^.addrOffset) $ do
let block_map = Map.fromList [ (labelIndex (blockLabel b), b) | b <- bs ]
-- Add block region to blocks.
let br = BlockRegion { brSize = next_ip^.addrOffset - addr^.addrOffset
, brBlocks = block_map
}
put $! s0 & blocks %~ Map.insert addr br
-}
{-
-- | Mark address as the start of a code block.
markCodeAddrBlock :: ArchConstraints arch
=> CodeAddrReason (ArchAddrWidth arch)
-- ^ Reason we are trying to disassemble starting from given address
-> ArchSegmentedAddr arch
-- ^ Address to start disassembling
-> AbsBlockState (ArchReg arch)
-- ^ Abstract block state at start of disassembly
-> CFGM arch ids ()
markCodeAddrBlock rsn addr ab = do
s <- get
-- Lookup block just before this address
case Map.lookupLT addr (s^.blocks) of
-- If that block overlaps with the address
Just (l, br)
| segmentIndex (addrSegment addr) == segmentIndex (addrSegment l)
, addr^.addrOffset < l^.addrOffset + brSize br -> do
-- Get block for addr
tryDisassembleAddr addr ab
-- Get block for old block
case Map.lookup l (s^.foundAddrs) of
Just info ->
tryDisassembleAddr l (foundAbstractState info)
Nothing -> error $ "Internal mark code addr as block saved but no reason information stored."
-- It's possible this will cause the current block to be broken, or cause a function to
-- boundaries. However, we don't think this should cause the need automatically to
-- re-evaluate a block as any information discovered should be strictly less than
-- the longer block.
_ -> do
tryDisassembleAddr addr ab
-}
------------------------------------------------------------------------
-- Transfer stmts
transferStmt :: ( RegisterInfo (ArchReg arch)
, HasRepr (ArchReg arch) TypeRepr
, MemWidth (ArchAddrWidth arch)
)
=> ArchitectureInfo arch
-- | Given a statement this modifies the processor state based on the statement.
absEvalStmt :: ArchitectureInfo arch
-> Stmt arch ids
-> State (AbsProcessorState (ArchReg arch) ids) ()
transferStmt info stmt =
absEvalStmt info stmt = withArchConstraints info $
case stmt of
AssignStmt a -> do
AssignStmt a ->
modify $ addAssignment info a
WriteMem addr memRepr v -> do
modify $ \r -> addMemWrite (r^.absInitialRegs^.curIP) addr memRepr v r
_ -> return ()
WriteMem addr memRepr v ->
modify $ addMemWrite addr memRepr v
PlaceHolderStmt{} ->
pure ()
Comment{} ->
pure ()
ExecArchStmt astmt ->
modify $ \r -> absEvalArchStmt info r astmt
newtype HexWord = HexWord Word64
instance Show HexWord where
showsPrec _ (HexWord w) = showHex w
-- | Mark a escaped code pointer as a function entry.
markAddrAsFunction :: ArchConstraints arch
=> CodeAddrReason (ArchAddrWidth arch)
-> ArchSegmentedAddr arch
-> CFGM arch ids ()
markAddrAsFunction rsn addr = do
s <- get
when (not (Set.member addr (s^.functionEntries))) $ do
let _high = Set.lookupGT addr (s^.functionEntries)
modify $ (functionEntries %~ Set.insert addr)
. (function_frontier %~ Map.insert addr rsn)
transferStmts :: ( HasRepr (ArchReg arch) TypeRepr
, RegisterInfo (ArchReg arch)
, MemWidth (ArchAddrWidth arch)
)
=> ArchitectureInfo arch
absEvalStmts :: ArchitectureInfo arch
-> AbsProcessorState (ArchReg arch) ids
-> [Stmt arch ids]
-> AbsProcessorState (ArchReg arch) ids
transferStmts info r stmts = execState (mapM_ (transferStmt info) stmts) r
absEvalStmts info r stmts = execState (mapM_ (absEvalStmt info) stmts) r
-- | Generate map that maps each assignment in the CFG to the abstract value
-- associated with it.
assignmentAbsValues :: forall arch ids
. ( HasRepr (ArchReg arch) TypeRepr
, RegisterInfo (ArchReg arch)
, MemWidth (ArchAddrWidth arch)
)
=> ArchitectureInfo arch
. ArchitectureInfo arch
-> Memory (ArchAddrWidth arch)
-> CFG arch ids
-> Map (ArchSegmentedAddr arch) (AbsBlockState (ArchReg arch))
@ -411,7 +319,7 @@ assignmentAbsValues info mem g absm =
-> MapF (AssignId ids) (ArchAbsValue arch)
-> MapF (AssignId ids) (ArchAbsValue arch)
insBlock b r0 m0 =
let final = transferStmts info r0 (blockStmts b)
let final = absEvalStmts info r0 (blockStmts b)
m = MapF.union (final^.absAssignments) m0 in
case blockTerm b of
Branch _ lb rb -> do
@ -429,19 +337,19 @@ assignmentAbsValues info mem g absm =
-- | Joins in the new abstract state and returns the locations for
-- which the new state is changed.
mergeIntraJump :: ArchConstraints arch
=> ArchSegmentedAddr arch
mergeIntraJump :: ArchSegmentedAddr arch
-- ^ Source label that we are jumping from.
-> AbsBlockState (ArchReg arch)
-- ^ Block state after executing instructions.
-> ArchSegmentedAddr arch
-- ^ Address we are trying to reach.
-> FunM arch ids ()
mergeIntraJump src ab _tgt
| not (absStackHasReturnAddr ab)
, debug DCFG ("WARNING: Missing return value in jump from " ++ show src ++ " to\n" ++ show ab) False
= error "internal: Unexpected mergeIntraJump"
mergeIntraJump src ab tgt = do
info <- liftCFG $ gets archInfo
withArchConstraints info $ do
when (not (absStackHasReturnAddr ab)) $ do
debug DCFG ("WARNING: Missing return value in jump from " ++ show src ++ " to\n" ++ show ab) $
pure ()
let rsn = NextIP src
-- Associate a new abstract state with the code region.
s0 <- use curFunInfo
@ -460,7 +368,6 @@ mergeIntraJump src ab tgt = do
Nothing -> do
curFunInfo . reverseEdges %= Map.insertWith Set.union tgt (Set.singleton src)
frontier %= Set.insert tgt
-- liftCFG $ markCodeAddrBlock rsn tgt ab
let found_info = FoundAddr { foundReason = rsn
, foundAbstractState = ab
}
@ -509,21 +416,17 @@ showJumpTableBoundsError err =
-- Returns the index bounds for a jump table of 'Nothing' if this is not a block
-- table.
getJumpTableBounds :: ( OrdF (ArchReg a)
, ShowF (ArchReg a)
, MemWidth (ArchAddrWidth a)
)
=> ArchitectureInfo a
getJumpTableBounds :: ArchitectureInfo a
-> AbsProcessorState (ArchReg a) ids -- ^ Current processor registers.
-> ArchSegmentedAddr a -- ^ Base
-> BVValue a ids (ArchAddrWidth a) -- ^ Index in jump table
-> Either (JumpTableBoundsError a ids) (ArchAddr a)
-- ^ One past last index in jump table or nothing
getJumpTableBounds arch regs base jump_index =
getJumpTableBounds info regs base jump_index = withArchConstraints info $
case transferValue regs jump_index of
StridedInterval (SI.StridedInterval _ index_base index_range index_stride) -> do
let index_end = index_base + (index_range + 1) * index_stride
if rangeInReadonlySegment base (jumpTableEntrySize arch * fromInteger index_end) then
if rangeInReadonlySegment base (jumpTableEntrySize info * fromInteger index_end) then
case Jmp.unsignedUpperBound (regs^.indexBounds) jump_index of
Right (Jmp.IntegerUpperBound bnd) | bnd == index_range -> Right $! fromInteger index_end
Right bnd -> Left (UpperBoundMismatch bnd index_range)
@ -582,20 +485,16 @@ newFunctionAddrs = lens _newFunctionAddrs (\s v -> s { _newFunctionAddrs = v })
-- | Mark addresses written to memory that point to code as function entry points.
recordWriteStmt :: ( HasRepr (ArchReg arch) TypeRepr
, MemWidth (ArchAddrWidth arch)
, OrdF (ArchReg arch)
, ShowF (ArchReg arch)
)
=> ArchitectureInfo arch
-> Memory (ArchAddrWidth arch)
-> AbsProcessorState (ArchReg arch) ids
-> Stmt arch ids
-> State (ParseState arch ids) ()
recordWriteStmt :: ArchitectureInfo arch
-> Memory (ArchAddrWidth arch)
-> AbsProcessorState (ArchReg arch) ids
-> Stmt arch ids
-> State (ParseState arch ids) ()
recordWriteStmt arch_info mem regs stmt = do
case stmt of
WriteMem _addr repr v
| Just Refl <- testEquality repr (addrMemRepr arch_info) -> do
withArchConstraints arch_info $ do
let addrs = concretizeAbsCodePointers mem (transferValue regs v)
writtenCodeAddrs %= (addrs ++)
_ -> return ()
@ -674,8 +573,7 @@ addrMemRepr arch_info =
-- | This parses a block that ended with a fetch and execute instruction.
parseFetchAndExecute :: forall arch ids
. ArchConstraints arch
=> ParseContext arch ids
. ParseContext arch ids
-> ArchLabel arch
-> [Stmt arch ids]
-> AbsProcessorState (ArchReg arch) ids
@ -687,10 +585,11 @@ parseFetchAndExecute ctx lbl stmts regs s' = do
let lbl_idx = labelIndex lbl
let mem = pctxMemory ctx
let arch_info = pctxArchInfo ctx
withArchConstraints arch_info $ do
-- See if next statement appears to end with a call.
-- We define calls as statements that end with a write that
-- stores the pc to an address.
let regs' = transferStmts arch_info regs stmts
let regs' = absEvalStmts arch_info regs stmts
case () of
-- The last statement was a call.
-- Note that in some cases the call is known not to return, and thus
@ -841,8 +740,7 @@ parseFetchAndExecute ctx lbl stmts regs s' = do
-- | This evalutes the statements in a block to expand the information known
-- about control flow targets of this block.
parseBlocks :: ArchConstraints arch
=> ParseContext arch ids
parseBlocks :: ParseContext arch ids
-- ^ Context for parsing blocks.
-> [(Block arch ids, AbsProcessorState (ArchReg arch) ids)]
-- ^ Queue of blocks to travese
@ -851,6 +749,7 @@ parseBlocks _ct [] = pure ()
parseBlocks ctx ((b,regs):rest) = do
let mem = pctxMemory ctx
let arch_info = pctxArchInfo ctx
withArchConstraints arch_info $ do
let lbl = blockLabel b
-- Assert we are still in source block.
assert (pctxAddr ctx == labelAddr lbl) $ do
@ -860,7 +759,7 @@ parseBlocks ctx ((b,regs):rest) = do
-- FIXME: we should propagate c back to the initial block, not just b
case blockTerm b of
Branch c lb rb -> do
let regs' = transferStmts arch_info regs (blockStmts b)
let regs' = absEvalStmts arch_info regs (blockStmts b)
mapM_ (recordWriteStmt arch_info mem regs') (blockStmts b)
let l = tryLookupBlock "left branch" src block_map lb
@ -872,8 +771,8 @@ parseBlocks ctx ((b,regs):rest) = do
-- tracking what (if anything) changed. We also might
-- need to keep going back and forth until we reach a
-- fixpoint
let l_regs' = transferStmts arch_info l_regs (blockStmts b)
let r_regs' = transferStmts arch_info r_regs (blockStmts b)
let l_regs' = absEvalStmts arch_info l_regs (blockStmts b)
let r_regs' = absEvalStmts arch_info r_regs (blockStmts b)
let pb = ParsedBlock { pblockLabel = idx
@ -886,7 +785,7 @@ parseBlocks ctx ((b,regs):rest) = do
parseBlocks ctx ((l, l_regs'):(r, r_regs'):rest)
Syscall s' -> do
let regs' = transferStmts arch_info regs (blockStmts b)
let regs' = absEvalStmts arch_info regs (blockStmts b)
mapM_ (recordWriteStmt arch_info mem regs') (blockStmts b)
let abst = finalAbsBlockState regs' s'
case concretizeAbsCodePointers mem (abst^.absRegState^.curIP) of
@ -913,7 +812,7 @@ parseBlocks ctx ((b,regs):rest) = do
-- Do nothing when this block ends in a translation error.
TranslateError _ msg -> do
let regs' = transferStmts arch_info regs (blockStmts b)
let regs' = absEvalStmts arch_info regs (blockStmts b)
let pb = ParsedBlock { pblockLabel = idx
, pblockStmts = blockStmts b
, pblockState = regs'
@ -925,8 +824,7 @@ parseBlocks ctx ((b,regs):rest) = do
-- | This evalutes the statements in a block to expand the information known
-- about control flow targets of this block.
transferBlocks :: ArchConstraints arch
=> BlockRegion arch ids
transferBlocks :: BlockRegion arch ids
-- ^ Input block regions
-> AbsProcessorState (ArchReg arch) ids
-- ^ Abstract state describing machine state when block is encountered.
@ -960,8 +858,7 @@ transferBlocks br regs =
liftCFG $ mapM_ (markAddrAsFunction (CallTarget src)) (ps^.newFunctionAddrs)
mapM_ (\(addr, abs_state) -> mergeIntraJump src abs_state addr) (ps^.intraJumpTargets)
transfer :: ArchConstraints arch
=> ArchSegmentedAddr arch
transfer :: ArchSegmentedAddr arch
-> FunM arch ids ()
transfer addr = do
mfinfo <- use $ curFunInfo . foundAddrs . at addr
@ -987,6 +884,8 @@ transfer addr = do
Nothing -> do
pure ()
withArchConstraints info $ do
assert (segmentIndex (addrSegment next_ip) == segmentIndex (addrSegment addr)) $ do
assert (next_ip^.addrOffset > addr^.addrOffset) $ do
let block_map = Map.fromList [ (labelIndex (blockLabel b), b) | b <- bs ]
@ -999,7 +898,7 @@ transfer addr = do
-- Main loop
-- | Explore a specific function
explore_fun_loop :: ArchConstraints arch => FunM arch ids ()
explore_fun_loop :: FunM arch ids ()
explore_fun_loop = do
st <- FunM get
case Set.minView (st^.frontier) of
@ -1009,8 +908,7 @@ explore_fun_loop = do
transfer addr
explore_fun_loop
explore_fun :: ArchConstraints arch
=> ArchSegmentedAddr arch
explore_fun :: ArchSegmentedAddr arch
-> CodeAddrReason (ArchAddrWidth arch)
-> CFGM arch ids ()
explore_fun addr rsn = do
@ -1026,8 +924,7 @@ explore_fun addr rsn = do
fs <- execStateT (unFunM explore_fun_loop) fs0
funInfo %= Map.insert addr (fs^.curFunInfo)
explore_frontier :: ArchConstraints arch
=> CFGM arch ids ()
explore_frontier :: CFGM arch ids ()
explore_frontier = do
st <- get
-- If local block frontier is empty, then try function frontier.
@ -1038,12 +935,6 @@ explore_frontier = do
explore_fun addr rsn
explore_frontier
-- | This returns true if the address is writable and value, and points to code.
memIsDataCodePointer :: Memory w -> SegmentedAddr w -> SegmentedAddr w -> Bool
memIsDataCodePointer _ a v
= segmentFlags (addrSegment v) `Perm.hasPerm` Perm.execute
&& segmentFlags (addrSegment a) `Perm.hasPerm` Perm.write
-- | Map from addresses to the associated symbol name.
type SymbolNameMap w = Map (SegmentedAddr w) BSC.ByteString
@ -1065,11 +956,16 @@ checkSymbolMap symbols = do
(c:_) | isDigit c -> Left "Symbol name that starts with a digit."
| otherwise -> Right ()
-- | This returns true if the address is writable and value is executable.
isDataCodePointer :: SegmentedAddr w -> SegmentedAddr w -> Bool
isDataCodePointer a v
= segmentFlags (addrSegment a) `Perm.hasPerm` Perm.write
&& segmentFlags (addrSegment v) `Perm.hasPerm` Perm.execute
-- | Construct a discovery info by starting with exploring from a given set of
-- function entry points.
cfgFromAddrs :: forall arch
. ArchConstraints arch
=> ArchitectureInfo arch
. ArchitectureInfo arch
-- ^ Architecture-specific information needed for doing control-flow exploration.
-> Memory (ArchAddrWidth arch)
-- ^ Memory to use when decoding instructions.
@ -1086,7 +982,7 @@ cfgFromAddrs :: forall arch
cfgFromAddrs arch_info mem symbols init_addrs mem_words =
runCFGM arch_info mem symbols $ do
case checkSymbolMap symbols of
Left msg -> error $ "interna error in cfgFromAddrs:" ++ msg
Left msg -> error $ "internal error in cfgFromAddrs:" ++ msg
Right () -> pure ()
-- Set abstract state for initial functions
mapM_ (markAddrAsFunction InitAddr) init_addrs
@ -1096,7 +992,7 @@ cfgFromAddrs arch_info mem symbols init_addrs mem_words =
s <- get
let mem_addrs =
filter (uncurry (notAlreadyFunction s)) $
filter (uncurry (memIsDataCodePointer mem)) $
filter (uncurry isDataCodePointer) $
mem_words
mapM_ (\(src,val) -> markAddrAsFunction (CodePointerInMem src) val) mem_addrs
explore_frontier

16
src/Data/Macaw/Discovery/Info.hs
View File

@ -11,6 +11,7 @@ discovery.
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
@ -245,7 +246,7 @@ instance ArchConstraints arch
type ReverseEdgeMap arch = (Map (ArchSegmentedAddr arch) (Set (ArchSegmentedAddr arch)))
-- | Information discovered about a particular
-- | Information discovered about a particular function
data DiscoveryFunInfo arch ids
= DiscoveryFunInfo { discoveredFunAddr :: !(ArchSegmentedAddr arch)
-- ^ Address of function entry block.
@ -283,7 +284,7 @@ initDiscoveryFunInfo :: ArchitectureInfo arch
initDiscoveryFunInfo info mem symMap addr rsn =
let nm = fromMaybe (BSC.pack (show addr)) (Map.lookup addr symMap)
faddr = FoundAddr { foundReason = rsn
, foundAbstractState = fnBlockStateFn info mem addr
, foundAbstractState = mkInitialAbsState info mem addr
}
in DiscoveryFunInfo { discoveredFunAddr = addr
, discoveredFunName = nm
@ -325,10 +326,15 @@ data DiscoveryInfo arch ids
-- ^ Set of functions to explore next.
}
ppDiscoveryInfoBlocks :: ArchConstraints arch
=> DiscoveryInfo arch ids
withDiscoveryArchConstraints :: DiscoveryInfo arch ids
-> (ArchConstraints arch => a)
-> a
withDiscoveryArchConstraints dinfo = withArchConstraints (archInfo dinfo)
ppDiscoveryInfoBlocks :: DiscoveryInfo arch ids
-> Doc
ppDiscoveryInfoBlocks info = vcat (pretty <$> Map.elems (info^.funInfo))
ppDiscoveryInfoBlocks info = withDiscoveryArchConstraints info $
vcat (pretty <$> Map.elems (info^.funInfo))
-- | Empty interpreter state.
emptyDiscoveryInfo :: NonceGenerator (ST ids) ids

6
src/Data/Macaw/Types.hs
View File

@ -8,6 +8,7 @@
-- The type of machine words, including bit vectors and floating point
------------------------------------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
@ -197,3 +198,8 @@ floatTypeRepr fir = BVTypeRepr (floatInfoBits fir)
-- parameterized type value has some representative type such as a TypeRepr.
class HasRepr (f :: k -> *) (v :: k -> *) | f -> v where
typeRepr :: f tp -> v tp
typeWidth :: HasRepr f TypeRepr => f (BVType w) -> NatRepr w
typeWidth x =
case typeRepr x of
BVTypeRepr w -> w