mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-12-28 08:34:23 +03:00
Merge branch 'master' of github.com:GaloisInc/macaw
This commit is contained in:
Joe Hendrix
commit
6391a87db1
@ -21,6 +21,7 @@ single CFG.
|
||||
{-# LANGUAGE StandaloneDeriving #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# LANGUAGE AllowAmbiguousTypes #-}
|
||||
module Data.Macaw.CFG.Core
|
||||
( -- * Stmt level declarations
|
||||
Stmt(..)
|
||||
@ -358,9 +359,15 @@ asBaseOffset x
|
||||
|
||||
class IPAlignment arch where
|
||||
-- | Take an aligned value and strip away the bits of the semantics that
|
||||
-- align it, leaving behind a (potentially unaligned) value.
|
||||
-- align it, leaving behind a (potentially unaligned) value. Return 'Nothing'
|
||||
-- if the input value does not appear to be a valid value for the instruction
|
||||
-- pointer.
|
||||
fromIPAligned :: ArchAddrValue arch ids -> Maybe (ArchAddrValue arch ids)
|
||||
|
||||
-- | Take an unaligned memory address and clean it up so that it is a valid
|
||||
-- value for the instruction pointer.
|
||||
toIPAligned :: MemAddr (ArchAddrWidth arch) -> MemAddr (ArchAddrWidth arch)
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- RegState
|
||||
|
||||
|
||||
@ -166,6 +166,15 @@ rewriteApp app = do
|
||||
f' <- rewriteApp (Trunc f w)
|
||||
rewriteApp $ Mux (BVTypeRepr w) c t' f'
|
||||
|
||||
Trunc (valueAsApp -> Just (UExt v _)) w -> case compareNat w (typeWidth v) of
|
||||
NatLT _ -> rewriteApp $ Trunc v w
|
||||
NatEQ -> pure v
|
||||
NatGT _ -> rewriteApp $ UExt v w
|
||||
Trunc (valueAsApp -> Just (SExt v _)) w -> case compareNat w (typeWidth v) of
|
||||
NatLT _ -> rewriteApp $ Trunc v w
|
||||
NatEQ -> pure v
|
||||
NatGT _ -> rewriteApp $ SExt v w
|
||||
|
||||
SExt (BVValue u x) w -> do
|
||||
pure $ BVValue w $ toUnsigned w $ toSigned u x
|
||||
UExt (BVValue _ x) w -> do
|
||||
@ -281,13 +290,116 @@ rewriteApp app = do
|
||||
|
||||
BVUnsignedLe (BVValue w x) (BVValue _ y) -> do
|
||||
pure $ boolLitValue $ toUnsigned w x <= toUnsigned w y
|
||||
-- in uext(x) <= uext(y) we can eliminate one or both uext's.
|
||||
-- same for sext's, even with unsigned comparisons!
|
||||
-- uext(x) <= yc = true if yc >= 2^width(x)-1
|
||||
-- uext(x) <= yc = x <= yc if yc < 2^width(x)-1
|
||||
-- similar shortcuts exist for the other inequalities
|
||||
BVUnsignedLe (BVValue _ x) (valueAsApp -> Just (UExt y _)) -> do
|
||||
let wShort = typeWidth y
|
||||
if x <= maxUnsigned wShort
|
||||
then rewriteApp (BVUnsignedLe (BVValue wShort x) y)
|
||||
else pure $ boolLitValue False
|
||||
BVUnsignedLe (valueAsApp -> Just (UExt x _)) (BVValue _ y) -> do
|
||||
let wShort = typeWidth x
|
||||
if y < maxUnsigned wShort
|
||||
then rewriteApp (BVUnsignedLe x (BVValue wShort y))
|
||||
else pure $ boolLitValue True
|
||||
BVUnsignedLe (valueAsApp -> Just (UExt x _)) (valueAsApp -> Just (UExt y _)) -> do
|
||||
let wx = typeWidth x
|
||||
wy = typeWidth y
|
||||
case compareNat wx wy of
|
||||
NatLT _ -> rewriteApp (UExt x wy) >>= \x' -> rewriteApp (BVUnsignedLe x' y)
|
||||
NatEQ -> rewriteApp (BVUnsignedLe x y)
|
||||
NatGT _ -> rewriteApp (UExt y wx) >>= \y' -> rewriteApp (BVUnsignedLe x y')
|
||||
BVUnsignedLe (valueAsApp -> Just (SExt x _)) (valueAsApp -> Just (SExt y _)) -> do
|
||||
let wx = typeWidth x
|
||||
wy = typeWidth y
|
||||
case compareNat wx wy of
|
||||
NatLT _ -> rewriteApp (SExt x wy) >>= \x' -> rewriteApp (BVUnsignedLe x' y)
|
||||
NatEQ -> rewriteApp (BVUnsignedLe x y)
|
||||
NatGT _ -> rewriteApp (SExt y wx) >>= \y' -> rewriteApp (BVUnsignedLe x y')
|
||||
|
||||
BVUnsignedLt (BVValue w x) (BVValue _ y) -> do
|
||||
pure $ boolLitValue $ toUnsigned w x < toUnsigned w y
|
||||
BVUnsignedLt (BVValue _ x) (valueAsApp -> Just (UExt y _)) -> do
|
||||
let wShort = typeWidth y
|
||||
if x < maxUnsigned wShort
|
||||
then rewriteApp (BVUnsignedLt (BVValue wShort x) y)
|
||||
else pure $ boolLitValue False
|
||||
BVUnsignedLt (valueAsApp -> Just (UExt x _)) (BVValue _ y) -> do
|
||||
let wShort = typeWidth x
|
||||
if y <= maxUnsigned wShort
|
||||
then rewriteApp (BVUnsignedLt x (BVValue wShort y))
|
||||
else pure $ boolLitValue True
|
||||
BVUnsignedLt (valueAsApp -> Just (UExt x _)) (valueAsApp -> Just (UExt y _)) -> do
|
||||
let wx = typeWidth x
|
||||
wy = typeWidth y
|
||||
case compareNat wx wy of
|
||||
NatLT _ -> rewriteApp (UExt x wy) >>= \x' -> rewriteApp (BVUnsignedLt x' y)
|
||||
NatEQ -> rewriteApp (BVUnsignedLt x y)
|
||||
NatGT _ -> rewriteApp (UExt y wx) >>= \y' -> rewriteApp (BVUnsignedLt x y')
|
||||
BVUnsignedLt (valueAsApp -> Just (SExt x _)) (valueAsApp -> Just (SExt y _)) -> do
|
||||
let wx = typeWidth x
|
||||
wy = typeWidth y
|
||||
case compareNat wx wy of
|
||||
NatLT _ -> rewriteApp (SExt x wy) >>= \x' -> rewriteApp (BVUnsignedLt x' y)
|
||||
NatEQ -> rewriteApp (BVUnsignedLt x y)
|
||||
NatGT _ -> rewriteApp (SExt y wx) >>= \y' -> rewriteApp (BVUnsignedLt x y')
|
||||
|
||||
BVSignedLe (BVValue w x) (BVValue _ y) -> do
|
||||
pure $ boolLitValue $ toSigned w x <= toSigned w y
|
||||
BVSignedLe (BVValue w x) (valueAsApp -> Just (SExt y _)) -> do
|
||||
let wShort = typeWidth y
|
||||
xv = toSigned w x
|
||||
if xv <= minSigned wShort
|
||||
then pure $ boolLitValue True
|
||||
else if xv > maxSigned wShort
|
||||
then pure $ boolLitValue False
|
||||
else rewriteApp (BVSignedLe (BVValue wShort x) y)
|
||||
BVSignedLe (valueAsApp -> Just (SExt x _)) (BVValue w y) -> do
|
||||
let wShort = typeWidth x
|
||||
yv = toSigned w y
|
||||
if yv < minSigned wShort
|
||||
then pure $ boolLitValue False
|
||||
else if yv >= maxSigned wShort
|
||||
then pure $ boolLitValue True
|
||||
else rewriteApp (BVSignedLe x (BVValue wShort y))
|
||||
BVSignedLe (valueAsApp -> Just (SExt x _)) (valueAsApp -> Just (SExt y _)) -> do
|
||||
let wx = typeWidth x
|
||||
wy = typeWidth y
|
||||
case compareNat wx wy of
|
||||
NatLT _ -> rewriteApp (SExt x wy) >>= \x' -> rewriteApp (BVUnsignedLe x' y)
|
||||
NatEQ -> rewriteApp (BVUnsignedLe x y)
|
||||
NatGT _ -> rewriteApp (SExt y wx) >>= \y' -> rewriteApp (BVUnsignedLe x y')
|
||||
-- for signed comparisons, uext(x) <= uext(y) is not necessarily equivalent
|
||||
-- to either x <= uext(y) or uext(x) <= y, so no rewrite for that!
|
||||
|
||||
BVSignedLt (BVValue w x) (BVValue _ y) -> do
|
||||
pure $ boolLitValue $ toSigned w x < toSigned w y
|
||||
BVSignedLt (BVValue w x) (valueAsApp -> Just (SExt y _)) -> do
|
||||
let wShort = typeWidth y
|
||||
xv = toSigned w x
|
||||
if xv < minSigned wShort
|
||||
then pure $ boolLitValue True
|
||||
else if xv >= maxSigned wShort
|
||||
then pure $ boolLitValue False
|
||||
else rewriteApp (BVSignedLt (BVValue wShort x) y)
|
||||
BVSignedLt (valueAsApp -> Just (SExt x _)) (BVValue w y) -> do
|
||||
let wShort = typeWidth x
|
||||
yv = toSigned w y
|
||||
if yv <= minSigned wShort
|
||||
then pure $ boolLitValue False
|
||||
else if yv > maxSigned wShort
|
||||
then pure $ boolLitValue True
|
||||
else rewriteApp (BVSignedLt x (BVValue wShort y))
|
||||
BVSignedLt (valueAsApp -> Just (SExt x _)) (valueAsApp -> Just (SExt y _)) -> do
|
||||
let wx = typeWidth x
|
||||
wy = typeWidth y
|
||||
case compareNat wx wy of
|
||||
NatLT _ -> rewriteApp (SExt x wy) >>= \x' -> rewriteApp (BVUnsignedLt x' y)
|
||||
NatEQ -> rewriteApp (BVUnsignedLt x y)
|
||||
NatGT _ -> rewriteApp (SExt y wx) >>= \y' -> rewriteApp (BVUnsignedLt x y')
|
||||
|
||||
BVTestBit (BVValue xw xc) (BVValue _ ic) | ic < min (natValue xw) (toInteger (maxBound :: Int)) -> do
|
||||
let v = xc `testBit` fromInteger ic
|
||||
|
||||
@ -800,7 +800,7 @@ parseFetchAndExecute ctx lbl_idx stmts regs s' = do
|
||||
let read_addr = relativeSegmentAddr (arBase arrayRead) & incAddr (arStride arrayRead * toInteger idx)
|
||||
in case readAddr mem endianness read_addr of
|
||||
Right tgt_addr
|
||||
| Just tgt_mseg <- asSegmentOff mem tgt_addr
|
||||
| Just tgt_mseg <- asSegmentOff mem (toIPAligned @arch tgt_addr)
|
||||
, Perm.isExecutable (segmentFlags (msegSegment tgt_mseg))
|
||||
-> Just tgt_mseg
|
||||
_ -> Nothing
|
||||
@ -810,7 +810,7 @@ parseFetchAndExecute ctx lbl_idx stmts regs s' = do
|
||||
Right shortOffset
|
||||
| Just offset <- extendDyn repr ext shortOffset
|
||||
, let tgt_addr = relativeSegmentAddr base & incAddr offset
|
||||
, Just tgt_mseg <- asSegmentOff mem tgt_addr
|
||||
, Just tgt_mseg <- asSegmentOff mem (toIPAligned @arch tgt_addr)
|
||||
, Perm.isExecutable (segmentFlags (msegSegment tgt_mseg))
|
||||
-> Just tgt_mseg
|
||||
_ -> Nothing
|
||||
|
||||
@ -855,7 +855,9 @@ type instance ArchStmt X86_64 = X86Stmt
|
||||
type instance ArchTermStmt X86_64 = X86TermStmt
|
||||
|
||||
-- x86 instructions can start at any byte
|
||||
instance IPAlignment X86_64 where fromIPAligned = Just
|
||||
instance IPAlignment X86_64 where
|
||||
fromIPAligned = Just
|
||||
toIPAligned = id
|
||||
|
||||
rewriteX86PrimFn :: X86PrimFn (Value X86_64 src) tp
|
||||
-> Rewriter X86_64 s src tgt (Value X86_64 tgt tp)
|
||||
|
||||
Loading…
Reference in New Issue
Block a user