mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-12-28 08:34:23 +03:00
Add support for adc/sbb.
This commit is contained in:
Joe Hendrix
parent
135add62ae
commit
5eaf2605ed
@ -589,36 +589,51 @@ uext (SomeStackOffset _) _ = TopV
|
||||
uext ReturnAddr _ = TopV
|
||||
uext TopV _ = TopV
|
||||
|
||||
asBoolConst :: AbsValue w BoolType -> Maybe Bool
|
||||
asBoolConst (BoolConst b) = Just b
|
||||
asBoolConst TopV = Nothing
|
||||
|
||||
bvadc :: forall w u
|
||||
. MemWidth w
|
||||
=> NatRepr u
|
||||
-> AbsValue w (BVType u)
|
||||
-> AbsValue w (BVType u)
|
||||
-> AbsValue w BoolType
|
||||
-> AbsValue w (BVType u)
|
||||
-- Stacks
|
||||
bvadc w (StackOffset a s) (FinSet t) c
|
||||
| [o0] <- Set.toList t
|
||||
, BoolConst b <- c
|
||||
, o <- if b then o0 + 1 else o0 =
|
||||
StackOffset a $ Set.map (fromInteger . addOff w o . toInteger) s
|
||||
bvadc w (FinSet t) (StackOffset a s) c
|
||||
| [o0] <- Set.toList t
|
||||
, BoolConst b <- c
|
||||
, o <- if b then o0 + 1 else o0 =
|
||||
StackOffset a $ Set.map (fromInteger . addOff w o . toInteger) s
|
||||
-- Strided intervals
|
||||
bvadc w v v' c
|
||||
| StridedInterval si1 <- v, StridedInterval si2 <- v' = go si1 si2
|
||||
| StridedInterval si <- v, IsFin s <- asFinSet "bvadc" v' = go si (SI.fromFoldable w s)
|
||||
| StridedInterval si <- v', IsFin s <- asFinSet "bvadc" v = go si (SI.fromFoldable w s)
|
||||
where
|
||||
go :: SI.StridedInterval u -> SI.StridedInterval u -> AbsValue w (BVType u)
|
||||
go si1 si2 = stridedInterval $ SI.bvadc w si1 si2 (asBoolConst c)
|
||||
|
||||
-- the rest
|
||||
bvadc _ (StackOffset ax _) _ _ = SomeStackOffset ax
|
||||
bvadc _ _ (StackOffset ax _) _ = SomeStackOffset ax
|
||||
bvadc _ (SomeStackOffset ax) _ _ = SomeStackOffset ax
|
||||
bvadc _ _ (SomeStackOffset ax) _ = SomeStackOffset ax
|
||||
bvadc _ _ _ _ = TopV
|
||||
|
||||
bvadd :: forall w u
|
||||
. MemWidth w
|
||||
=> NatRepr u
|
||||
-> AbsValue w (BVType u)
|
||||
-> AbsValue w (BVType u)
|
||||
-> AbsValue w (BVType u)
|
||||
-- Stacks
|
||||
bvadd w (StackOffset a s) (FinSet t) | [o] <- Set.toList t = do
|
||||
StackOffset a $ Set.map (fromInteger . addOff w o . toInteger) s
|
||||
bvadd w (FinSet t) (StackOffset a s) | [o] <- Set.toList t = do
|
||||
StackOffset a $ Set.map (fromInteger . addOff w o . toInteger) s
|
||||
-- Strided intervals
|
||||
bvadd w v v'
|
||||
| StridedInterval si1 <- v, StridedInterval si2 <- v' = go si1 si2
|
||||
| StridedInterval si <- v, IsFin s <- asFinSet "bvadd" v' = go si (SI.fromFoldable w s)
|
||||
| StridedInterval si <- v', IsFin s <- asFinSet "bvadd" v = go si (SI.fromFoldable w s)
|
||||
where
|
||||
go :: SI.StridedInterval u -> SI.StridedInterval u -> AbsValue w (BVType u)
|
||||
go si1 si2 = stridedInterval $ SI.bvadd w si1 si2
|
||||
|
||||
-- subvalues
|
||||
-- bvadd w (SubValue _n _av c) v' = bvadd w c v'
|
||||
-- bvadd w v (SubValue _n _av c) = bvadd w v c
|
||||
|
||||
-- the rest
|
||||
bvadd _ (StackOffset ax _) _ = SomeStackOffset ax
|
||||
bvadd _ _ (StackOffset ax _) = SomeStackOffset ax
|
||||
bvadd _ (SomeStackOffset ax) _ = SomeStackOffset ax
|
||||
bvadd _ _ (SomeStackOffset ax) = SomeStackOffset ax
|
||||
bvadd _ _ _ = TopV
|
||||
bvadd w x y = bvadc w x y (BoolConst False)
|
||||
|
||||
setL :: Ord a
|
||||
=> ([a] -> AbsValue w (BVType n))
|
||||
@ -628,6 +643,64 @@ setL :: Ord a
|
||||
setL def c l | length l > maxSetSize = def l
|
||||
| otherwise = c (Set.fromList l)
|
||||
|
||||
-- | Subtracting
|
||||
bvsbb :: forall w u
|
||||
. MemWidth w
|
||||
=> Memory w
|
||||
-- ^ Memory used for checking code pointers.
|
||||
-> NatRepr u
|
||||
-> AbsValue w (BVType u)
|
||||
-> AbsValue w (BVType u)
|
||||
-> AbsValue w BoolType
|
||||
-> AbsValue w (BVType u)
|
||||
bvsbb mem w (CodePointers s b) (FinSet t) (BoolConst False)
|
||||
-- If we just have zero.
|
||||
| Set.null s && b = FinSet (Set.map (toUnsigned w . negate) t)
|
||||
| all isJust vals && (not b || Set.singleton 0 == t) =
|
||||
CodePointers (Set.fromList (catMaybes vals)) b
|
||||
| otherwise = error "Losing code pointers due to bvsub."
|
||||
where vals :: [Maybe (MemSegmentOff w)]
|
||||
vals = do
|
||||
x <- Set.toList s
|
||||
y <- Set.toList t
|
||||
let z = relativeSegmentAddr x & incAddr (negate y)
|
||||
case asSegmentOff mem z of
|
||||
Just z_mseg | segmentFlags (msegSegment z_mseg) `Perm.hasPerm` Perm.execute ->
|
||||
pure (Just z_mseg)
|
||||
_ ->
|
||||
pure Nothing
|
||||
bvsbb _ _ xv@(CodePointers xs xb) (CodePointers ys yb) (BoolConst False)
|
||||
-- If we just have zero.
|
||||
| Set.null ys && yb = xv
|
||||
--
|
||||
| all isJust vals && xb == yb =
|
||||
if xb then
|
||||
FinSet (Set.insert 0 (Set.fromList (catMaybes vals)))
|
||||
else
|
||||
FinSet (Set.fromList (catMaybes vals))
|
||||
| otherwise = error "Losing code pointers due to bvsub."
|
||||
where vals :: [Maybe Integer]
|
||||
vals = do
|
||||
x <- Set.toList xs
|
||||
y <- Set.toList ys
|
||||
pure (relativeSegmentAddr x `diffAddr` relativeSegmentAddr y)
|
||||
bvsbb _ w (FinSet s) (asFinSet "bvsub3" -> IsFin t) (BoolConst b) =
|
||||
setL (stridedInterval . SI.fromFoldable w) FinSet $ do
|
||||
x <- Set.toList s
|
||||
y <- Set.toList t
|
||||
return $ toUnsigned w $ (x - y) - (if b then 1 else 0)
|
||||
bvsbb _ w (StackOffset ax s) (asFinSet "bvsub6" -> IsFin t) (BoolConst False) =
|
||||
setL (\_ -> SomeStackOffset ax) (StackOffset ax) $ do
|
||||
x <- toInteger <$> Set.toList s
|
||||
y <- Set.toList t
|
||||
return $! fromInteger (toUnsigned w (x - y))
|
||||
bvsbb _ _ (StackOffset ax _) _ _ = SomeStackOffset ax
|
||||
bvsbb _ _ _ (StackOffset _ _) _ = TopV
|
||||
bvsbb _ _ (SomeStackOffset ax) _ _ = SomeStackOffset ax
|
||||
bvsbb _ _ _ (SomeStackOffset _) _ = TopV
|
||||
bvsbb _ _ _ _ _b = TopV -- Keep the pattern checker happy
|
||||
|
||||
|
||||
-- | Subtracting
|
||||
bvsub :: forall w u
|
||||
. MemWidth w
|
||||
@ -643,9 +716,6 @@ bvsub mem w (CodePointers s b) (FinSet t)
|
||||
| all isJust vals && (not b || Set.singleton 0 == t) =
|
||||
CodePointers (Set.fromList (catMaybes vals)) b
|
||||
| otherwise = error "Losing code pointers due to bvsub."
|
||||
-- TODO: Fix this.
|
||||
-- debug DAbsInt ("drooping " ++ show (ppIntegerSet s) ++ " " ++ show (ppIntegerSet t)) $
|
||||
-- setL (stridedInterval . SI.fromFoldable w) FinSet (toInteger <$> vals)
|
||||
where vals :: [Maybe (MemSegmentOff w)]
|
||||
vals = do
|
||||
x <- Set.toList s
|
||||
@ -666,9 +736,6 @@ bvsub _ _ xv@(CodePointers xs xb) (CodePointers ys yb)
|
||||
else
|
||||
FinSet (Set.fromList (catMaybes vals))
|
||||
| otherwise = error "Losing code pointers due to bvsub."
|
||||
-- TODO: Fix this.
|
||||
-- debug DAbsInt ("drooping " ++ show (ppIntegerSet s) ++ " " ++ show (ppIntegerSet t)) $
|
||||
-- setL (stridedInterval . SI.fromFoldable w) FinSet (toInteger <$> vals)
|
||||
where vals :: [Maybe Integer]
|
||||
vals = do
|
||||
x <- Set.toList xs
|
||||
@ -1211,21 +1278,26 @@ finalAbsBlockState c s =
|
||||
------------------------------------------------------------------------
|
||||
-- Transfer functions
|
||||
|
||||
transferApp :: ( RegisterInfo (ArchReg a)
|
||||
transferApp :: forall a ids tp
|
||||
. ( RegisterInfo (ArchReg a)
|
||||
, HasCallStack
|
||||
)
|
||||
=> AbsProcessorState (ArchReg a) ids
|
||||
-> App (Value a ids) tp
|
||||
-> ArchAbsValue a tp
|
||||
transferApp r a =
|
||||
transferApp r a = do
|
||||
let t :: Value a ids utp -> ArchAbsValue a utp
|
||||
t = transferValue r
|
||||
case a of
|
||||
Trunc v w -> trunc (transferValue r v) w
|
||||
UExt v w -> uext (transferValue r v) w
|
||||
BVAdd w x y -> bvadd w (transferValue r x) (transferValue r y)
|
||||
BVSub w x y -> bvsub (absMem r) w (transferValue r x) (transferValue r y)
|
||||
BVMul w x y -> bvmul w (transferValue r x) (transferValue r y)
|
||||
BVAnd w x y -> bvand w (transferValue r x) (transferValue r y)
|
||||
BVOr w x y -> bitop (.|.) w (transferValue r x) (transferValue r y)
|
||||
Trunc v w -> trunc (t v) w
|
||||
UExt v w -> uext (t v) w
|
||||
BVAdd w x y -> bvadd w (t x) (t y)
|
||||
BVAdc w x y c -> bvadc w (t x) (t y) (t c)
|
||||
BVSub w x y -> bvsub (absMem r) w (t x) (t y)
|
||||
BVSbb w x y b -> bvsbb (absMem r) w (t x) (t y) (t b)
|
||||
BVMul w x y -> bvmul w (t x) (t y)
|
||||
BVAnd w x y -> bvand w (t x) (t y)
|
||||
BVOr w x y -> bitop (.|.) w (t x) (t y)
|
||||
_ -> TopV
|
||||
|
||||
-- | Minimal information needed to parse a function call/system call
|
||||
@ -1259,8 +1331,9 @@ absEvalCall params ab0 addr =
|
||||
| Just Refl <- testEquality r ip_reg =
|
||||
CodePointers (Set.singleton addr) False
|
||||
| Just Refl <- testEquality r sp_reg =
|
||||
let w = type_width (typeRepr r)
|
||||
in bvadd w (ab0^.absRegState^.boundValue r) (FinSet (Set.singleton (postCallStackDelta params)))
|
||||
let w = typeWidth r
|
||||
in bvadd w (ab0^.absRegState^.boundValue r)
|
||||
(FinSet (Set.singleton (postCallStackDelta params)))
|
||||
-- Copy callee saved registers
|
||||
| preserveReg params r =
|
||||
ab0^.absRegState^.boundValue r
|
||||
|
||||
@ -84,7 +84,7 @@ refineApp app av regs =
|
||||
|
||||
-- FIXME: HACK
|
||||
-- This detects r - x < 0 || r - x == 0, i.e. r <= x
|
||||
OrApp (getAssignApp -> Just (UsbbOverflows _ r xv@(BVValue sz x) (BoolValue False)))
|
||||
OrApp (getAssignApp -> Just (UsbbOverflows r xv@(BVValue sz x) (BoolValue False)))
|
||||
(getAssignApp -> Just (Eq (getAssignApp -> Just (BVAdd _ r' y)) (BVValue _ 0)))
|
||||
| Just Refl <- testEquality r r'
|
||||
, Just Refl <- testEquality y (mkLit sz (negate x))
|
||||
@ -94,7 +94,7 @@ refineApp app av regs =
|
||||
-- FIXME: HACK
|
||||
-- This detects not (r - x < 0) && not (r - x == 0), i.e. x < r
|
||||
AndApp (getAssignApp -> Just
|
||||
(NotApp (getAssignApp -> Just (UsbbOverflows _ r xv@(BVValue sz x) (BoolValue False)))))
|
||||
(NotApp (getAssignApp -> Just (UsbbOverflows r xv@(BVValue sz x) (BoolValue False)))))
|
||||
(getAssignApp -> Just
|
||||
(NotApp (getAssignApp -> Just (Eq (getAssignApp -> Just (BVAdd _ r' y)) (BVValue _ 0)))))
|
||||
| Just Refl <- testEquality r r'
|
||||
|
||||
@ -24,7 +24,7 @@ module Data.Macaw.AbsDomain.StridedInterval
|
||||
-- Domain operations
|
||||
, lub, lubSingleton, glb
|
||||
-- Operations
|
||||
, bvadd, bvmul, trunc
|
||||
, bvadd, bvadc, bvmul, trunc
|
||||
-- Debugging
|
||||
) where
|
||||
|
||||
@ -336,16 +336,33 @@ bvadd sz si1 si2 =
|
||||
r | m == 0 = error "bvadd given 0 stride"
|
||||
| otherwise = (range si1 * (stride si1 `div` m)) + (range si2 * (stride si2 `div` m))
|
||||
|
||||
-- prop_bvadd :: StridedInterval (BVType 64)
|
||||
-- -> StridedInterval (BVType 64)
|
||||
-- -> Bool
|
||||
-- prop_bvadd = mk_prop (+) bvadd
|
||||
bvadc :: NatRepr u
|
||||
-> StridedInterval u
|
||||
-> StridedInterval u
|
||||
-> Maybe Bool
|
||||
-> StridedInterval u
|
||||
bvadc sz si1 si2 (Just b)
|
||||
| Just s <- isSingleton si1 =
|
||||
clamp sz $ si2 { base = base si2 + s + (if b then 1 else 0) }
|
||||
bvadc sz si1 si2 (Just b)
|
||||
| Just s <- isSingleton si2 =
|
||||
clamp sz $ si1 { base = base si1 + s + (if b then 1 else 0) }
|
||||
bvadc sz si1 si2 b =
|
||||
clamp sz $ StridedInterval { typ = typ si1
|
||||
, base = base si1 + base si2 + (if b == Just True then 1 else 0)
|
||||
, range = r
|
||||
, stride = m }
|
||||
where
|
||||
m | b == Nothing = 1
|
||||
| otherwise = gcd (stride si1) (stride si2)
|
||||
|
||||
-- We have (x + [0..a] * b) * (y + [0 .. d] * e)
|
||||
-- = (x * y) + [0..a] * b * y + [0 .. d] * e * x + ([0..a] * b * [0..d] * e)
|
||||
-- `subsetOf` (x * y) + [0..a] * (b * y)
|
||||
-- + 0 + [0 .. d] * (e * x)
|
||||
-- + 0 + ([0..a*d] * (b * e)
|
||||
-- The amount to increase the range by given b.
|
||||
-- We add 1 when b == Nothing due to the uncertainty
|
||||
b_off | b == Nothing = 1
|
||||
| otherwise = 0
|
||||
|
||||
r | m == 0 = error "bvadd given 0 stride"
|
||||
| otherwise = (range si1 * (stride si1 `div` m)) + (range si2 * (stride si2 `div` m) + b_off)
|
||||
|
||||
bvmul :: NatRepr u
|
||||
-> StridedInterval u
|
||||
|
||||
@ -68,9 +68,18 @@ data App (f :: Type -> *) (tp :: Type) where
|
||||
----------------------------------------------------------------------
|
||||
-- Bitvector operations
|
||||
|
||||
-- | @BVAdd w x y@ denotes @x + y@.
|
||||
BVAdd :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
|
||||
-- | @BVAdc w x y c@ denotes @x + y + (c ? 1 : 0)@.
|
||||
BVAdc :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> !(f BoolType) -> App f (BVType n)
|
||||
|
||||
-- | @BVSub w x y@ denotes @x - y@.
|
||||
BVSub :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
|
||||
-- | @BVSbb w x y b@ denotes @(x - y) - (b ? 1 : 0)@.
|
||||
BVSbb :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> !(f BoolType) -> App f (BVType n)
|
||||
|
||||
-- Multiply two numbers
|
||||
BVMul :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> !(f (BVType n)) -> App f (BVType n)
|
||||
|
||||
@ -112,32 +121,37 @@ data App (f :: Type -> *) (tp :: Type) where
|
||||
--
|
||||
-- This is the sum of three three values cannot be represented as an unsigned number.
|
||||
UadcOverflows :: (1 <= n)
|
||||
=> !(NatRepr n)
|
||||
-> !(f (BVType 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 :: (1 <= n)
|
||||
=> !(NatRepr n)
|
||||
-> !(f (BVType n))
|
||||
=> !(f (BVType n))
|
||||
-> !(f (BVType n))
|
||||
-> !(f BoolType)
|
||||
-> App f BoolType
|
||||
|
||||
-- Unsigned subtract with borrow overflow
|
||||
--
|
||||
-- @UsbbOverflows w x y c@ should be true iff the result
|
||||
-- @(toNat x - toNat y) - (c ? 1 : 0)@ is not between @0@ and @2^w-1@.
|
||||
-- Since everything is unsigned, this is equivalent to @x unsignedLt (y + (c ? 1 : 0)@.
|
||||
UsbbOverflows :: (1 <= n)
|
||||
=> !(NatRepr n)
|
||||
-> !(f (BVType n))
|
||||
=> !(f (BVType n))
|
||||
-> !(f (BVType n))
|
||||
-> !(f BoolType)
|
||||
-> App f BoolType
|
||||
|
||||
-- Signed subtract with borrow overflow
|
||||
-- Signed subtract with borrow overflow.
|
||||
--
|
||||
-- @SsbbOverflows w x y c@ should be true iff the result
|
||||
-- @(toInt x - toInt y) - (c ? 1 : 0)@ is not between @-2^(w-1)@ and @2^(w-1)-1@.
|
||||
-- An equivalent way to express this is that x and y should have opposite signs and
|
||||
-- the sign of the result should differ from the sign of x.
|
||||
SsbbOverflows :: (1 <= n)
|
||||
=> !(NatRepr n)
|
||||
-> !(f (BVType n))
|
||||
=> !(f (BVType n))
|
||||
-> !(f (BVType n))
|
||||
-> !(f BoolType)
|
||||
-> App f BoolType
|
||||
@ -159,8 +173,9 @@ data App (f :: Type -> *) (tp :: Type) where
|
||||
|
||||
-- | bsf "bit scan forward" returns the index of the
|
||||
-- most-significant bit that is 1. An equivalent way of stating
|
||||
-- this is that it returns the number "least" zero-bits. This
|
||||
-- returns n if the value is zero.
|
||||
-- this is that it returns the number zero-bits starting from
|
||||
-- the most-significant bit location. This returns n if the
|
||||
-- value is zero.
|
||||
Bsr :: (1 <= n) => !(NatRepr n) -> !(f (BVType n)) -> App f (BVType n)
|
||||
|
||||
----------------------------------------------------------------------
|
||||
@ -328,8 +343,10 @@ ppAppA pp a0 =
|
||||
OrApp x y -> sexprA "or" [ pp x, pp y ]
|
||||
NotApp x -> sexprA "not" [ pp x ]
|
||||
XorApp x y -> sexprA "xor" [ pp x, pp y ]
|
||||
BVAdd _ x y -> sexprA "bv_add" [ pp x, pp y ]
|
||||
BVAdd _ x y -> sexprA "bv_add" [ pp x, pp y ]
|
||||
BVAdc _ x y c -> sexprA "bv_adc" [ pp x, pp y, pp c ]
|
||||
BVSub _ x y -> sexprA "bv_sub" [ pp x, pp y ]
|
||||
BVSbb _ x y b -> sexprA "bv_sbb" [ pp x, pp y, pp b ]
|
||||
BVMul _ x y -> sexprA "bv_mul" [ pp x, pp y ]
|
||||
BVUnsignedLt x y -> sexprA "bv_ult" [ pp x, pp y ]
|
||||
BVUnsignedLe x y -> sexprA "bv_ule" [ pp x, pp y ]
|
||||
@ -346,10 +363,10 @@ ppAppA pp a0 =
|
||||
Eq x y -> sexprA "eq" [ pp x, pp y ]
|
||||
PopCount _ x -> sexprA "popcount" [ 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 ]
|
||||
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 ]
|
||||
|
||||
@ -386,8 +403,10 @@ instance HasRepr (App f) TypeRepr where
|
||||
NotApp{} -> knownType
|
||||
XorApp{} -> knownType
|
||||
|
||||
BVAdd w _ _ -> BVTypeRepr w
|
||||
BVSub w _ _ -> BVTypeRepr w
|
||||
BVAdd w _ _ -> BVTypeRepr w
|
||||
BVAdc w _ _ _ -> BVTypeRepr w
|
||||
BVSub w _ _ -> BVTypeRepr w
|
||||
BVSbb w _ _ _ -> BVTypeRepr w
|
||||
BVMul w _ _ -> BVTypeRepr w
|
||||
|
||||
BVUnsignedLt{} -> knownType
|
||||
|
||||
@ -513,22 +513,22 @@ instance S.IsValue (Expr ids) where
|
||||
|
||||
uadc_overflows x y c
|
||||
| Just 0 <- asBVLit y, Just False <- asBoolLit c = S.false
|
||||
| otherwise = app $ UadcOverflows (typeWidth x) x y c
|
||||
| otherwise = app $ UadcOverflows x y c
|
||||
sadc_overflows x y c
|
||||
| Just 0 <- asBVLit y, Just False <- asBoolLit c = S.false
|
||||
| otherwise = app $ SadcOverflows (typeWidth x) x y c
|
||||
| otherwise = app $ SadcOverflows x y c
|
||||
|
||||
usbb_overflows x y c
|
||||
| Just 0 <- asBVLit y, Just False <- asBoolLit c = S.false
|
||||
-- If the borrow bit is zero, this is equivalent to unsigned x < y.
|
||||
| Just False <- asBoolLit c = S.bvUlt x y
|
||||
| otherwise = app $ UsbbOverflows (typeWidth x) x y c
|
||||
| otherwise = app $ UsbbOverflows x y c
|
||||
|
||||
ssbb_overflows x y c
|
||||
| Just 0 <- asBVLit y, Just False <- asBoolLit c = S.false
|
||||
-- If the borrow bit is zero, this is equivalent to signed x < y.
|
||||
-- FIXME: not true? | Just 0 <- asBVLit c = app $ BVSignedLt x y
|
||||
| otherwise = app $ SsbbOverflows (typeWidth x) x y c
|
||||
| otherwise = app $ SsbbOverflows x y c
|
||||
|
||||
bsf x = app $ Bsf (typeWidth x) x
|
||||
bsr x = app $ Bsr (typeWidth x) x
|
||||
|
||||
Loading…
Reference in New Issue
Block a user