mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-11-29 21:44:11 +03:00
Merge branch 'master' of github.com:GaloisInc/macaw
This commit is contained in:
Iavor Diatchki
commit
62ae9ae130
@ -331,6 +331,8 @@ data Value arch ids tp
|
||||
. (tp ~ BVType n, 1 <= n)
|
||||
=> BVValue !(NatRepr n) !Integer
|
||||
-- ^ A constant bitvector
|
||||
--
|
||||
-- The integer should be between 0 and 2^n-1.
|
||||
| (tp ~ BoolType)
|
||||
=> BoolValue !Bool
|
||||
-- ^ A constant Boolean
|
||||
|
||||
@ -178,8 +178,6 @@ mkBlocksCFG archFns halloc memBaseVarMap nm posFn macawBlocks = do
|
||||
mkCrucCFG archFns halloc nm $ do
|
||||
addBlocksCFG archFns memBaseVarMap posFn macawBlocks
|
||||
|
||||
type FunBlockMap arch s = Map (M.ArchSegmentOff arch, Word64) (CR.Label s)
|
||||
|
||||
mkFunCFG :: forall s arch ids
|
||||
. MacawSymbolicArchFunctions arch
|
||||
-- ^ Architecture specific functions.
|
||||
@ -197,17 +195,17 @@ mkFunCFG :: forall s arch ids
|
||||
mkFunCFG archFns halloc memBaseVarMap nm posFn fn = do
|
||||
mkCrucCFG archFns halloc nm $ do
|
||||
let insSentences :: M.ArchSegmentOff arch
|
||||
-> (FunBlockMap arch s,Int)
|
||||
-> (BlockLabelMap arch s,Int)
|
||||
-> [M.StatementList arch ids]
|
||||
-> (FunBlockMap arch s,Int)
|
||||
-> (BlockLabelMap arch s,Int)
|
||||
insSentences _ m [] = m
|
||||
insSentences base (m,c) (s:r) =
|
||||
insSentences base
|
||||
(Map.insert (base,M.stmtsIdent s) (CR.Label c) m,c+1)
|
||||
(nextStatements (M.stmtsTerm s) ++ r)
|
||||
let insBlock :: (FunBlockMap arch s,Int) -> M.ParsedBlock arch ids -> (FunBlockMap arch s,Int)
|
||||
let insBlock :: (BlockLabelMap arch s,Int) -> M.ParsedBlock arch ids -> (BlockLabelMap arch s,Int)
|
||||
insBlock m b = insSentences (M.pblockAddr b) m [M.blockStatementList b]
|
||||
let blockLabelMap :: FunBlockMap arch s
|
||||
let blockLabelMap :: BlockLabelMap arch s
|
||||
blockLabelMap = fst $ foldl' insBlock (Map.empty,0) (Map.elems (fn^.M.parsedBlocks))
|
||||
let regReg = CR.Reg { CR.regPosition = posFn (M.discoveredFunAddr fn)
|
||||
, CR.regId = 0
|
||||
|
||||
@ -38,6 +38,7 @@ module Data.Macaw.Symbolic.CrucGen
|
||||
, MacawMonad
|
||||
, runMacawMonad
|
||||
, addMacawBlock
|
||||
, BlockLabelMap
|
||||
, addParsedBlock
|
||||
, nextStatements
|
||||
, valueToCrucible
|
||||
@ -738,8 +739,11 @@ setMachineRegs newRegs = do
|
||||
regReg <- gets crucRegisterReg
|
||||
addStmt $ CR.SetReg regReg newRegs
|
||||
|
||||
addMacawParsedTermStmt :: Map (M.ArchSegmentOff arch, Word64) (CR.Label s)
|
||||
-- ^ Map from block addresses to starting label
|
||||
-- | Map from block information to Crucible label (used to generate term statements)
|
||||
type BlockLabelMap arch s = Map (M.ArchSegmentOff arch, Word64) (CR.Label s)
|
||||
|
||||
addMacawParsedTermStmt :: BlockLabelMap arch s
|
||||
-- ^ Block label map for this function
|
||||
-> M.ArchSegmentOff arch
|
||||
-- ^ Address of this block
|
||||
-> M.ParsedTermStmt arch ids
|
||||
@ -760,8 +764,13 @@ addMacawParsedTermStmt blockLabelMap thisAddr tstmt = do
|
||||
M.ParsedJump regs nextAddr -> do
|
||||
setMachineRegs =<< createRegStruct regs
|
||||
addTermStmt $ CR.Jump (parsedBlockLabel blockLabelMap nextAddr 0)
|
||||
M.ParsedLookupTable _regs _idx _possibleAddrs -> do
|
||||
error "Crucible symbolic generator does not yet support lookup tables."
|
||||
M.ParsedLookupTable regs _idx _possibleAddrs -> do
|
||||
setMachineRegs =<< createRegStruct regs
|
||||
let cond = undefined
|
||||
-- TODO: Add ability in CrucGen to generate new labels and add new blocks.
|
||||
let tlbl = undefined
|
||||
let flbl = undefined
|
||||
addTermStmt $! CR.Br cond tlbl flbl
|
||||
M.ParsedReturn regs -> do
|
||||
regValues <- createRegStruct regs
|
||||
addTermStmt $ CR.Return regValues
|
||||
@ -771,7 +780,6 @@ addMacawParsedTermStmt blockLabelMap thisAddr tstmt = do
|
||||
let flbl = parsedBlockLabel blockLabelMap thisAddr (M.stmtsIdent f)
|
||||
addTermStmt $! CR.Br crucCond tlbl flbl
|
||||
M.ParsedArchTermStmt aterm regs _mret -> do
|
||||
archFns <- gets translateFns
|
||||
crucGenArchTermStmt archFns aterm regs
|
||||
M.ParsedTranslateError msg -> do
|
||||
msgVal <- crucibleValue (C.TextLit msg)
|
||||
@ -789,7 +797,7 @@ nextStatements tstmt =
|
||||
addStatementList :: MacawSymbolicArchFunctions arch
|
||||
-> MemSegmentMap (M.ArchAddrWidth arch)
|
||||
-- ^ Base address map
|
||||
-> Map (M.ArchSegmentOff arch, Word64) (CR.Label s)
|
||||
-> BlockLabelMap arch s
|
||||
-- ^ Map from block index to Crucible label
|
||||
-> M.ArchSegmentOff arch
|
||||
-- ^ Address of block that starts statements
|
||||
@ -822,7 +830,7 @@ addParsedBlock :: forall arch ids s
|
||||
. MacawSymbolicArchFunctions arch
|
||||
-> MemSegmentMap (M.ArchAddrWidth arch)
|
||||
-- ^ Base address map
|
||||
-> Map (M.ArchSegmentOff arch, Word64) (CR.Label s)
|
||||
-> BlockLabelMap arch s
|
||||
-- ^ Map from block index to Crucible label
|
||||
-> (M.ArchSegmentOff arch -> C.Position)
|
||||
-- ^ Function for generating position from offset from start of this block.
|
||||
@ -836,4 +844,5 @@ addParsedBlock tfns baseAddrMap blockLabelMap posFn regReg b = do
|
||||
let thisPosFn :: M.ArchAddrWord arch -> C.Position
|
||||
thisPosFn off = posFn r
|
||||
where Just r = M.incSegmentOff base (toInteger off)
|
||||
addStatementList tfns baseAddrMap blockLabelMap (M.pblockAddr b) thisPosFn regReg [(0, M.blockStatementList b)] []
|
||||
addStatementList tfns baseAddrMap blockLabelMap
|
||||
(M.pblockAddr b) thisPosFn regReg [(0, M.blockStatementList b)] []
|
||||
|
||||
@ -52,7 +52,8 @@ module Data.Macaw.X86.Generator
|
||||
, asApp
|
||||
, asArchFn
|
||||
, asBoolLit
|
||||
, asBVLit
|
||||
, asUnsignedBVLit
|
||||
, asSignedBVLit
|
||||
, eval
|
||||
, getRegValue
|
||||
, setReg
|
||||
@ -79,6 +80,7 @@ import Data.Maybe
|
||||
import Data.Parameterized.Classes
|
||||
import Data.Parameterized.Map (MapF)
|
||||
import qualified Data.Parameterized.Map as MapF
|
||||
import Data.Parameterized.NatRepr
|
||||
import Data.Parameterized.Nonce
|
||||
import Data.Parameterized.TraversableFC
|
||||
import Data.Sequence (Seq)
|
||||
@ -137,9 +139,15 @@ asBoolLit :: Expr ids BoolType -> Maybe Bool
|
||||
asBoolLit (ValueExpr (BoolValue b)) = Just b
|
||||
asBoolLit _ = Nothing
|
||||
|
||||
asBVLit :: Expr ids (BVType w) -> Maybe Integer
|
||||
asBVLit (ValueExpr (BVValue _ v)) = Just v
|
||||
asBVLit _ = Nothing
|
||||
-- | If expression is a literal bitvector, then return as an unsigned integer.
|
||||
asUnsignedBVLit :: Expr ids (BVType w) -> Maybe Integer
|
||||
asUnsignedBVLit (ValueExpr (BVValue w v)) = Just (toUnsigned w v)
|
||||
asUnsignedBVLit _ = Nothing
|
||||
|
||||
-- | If expression is a literal bitvector, then return as an signed integer.
|
||||
asSignedBVLit :: Expr ids (BVType w) -> Maybe Integer
|
||||
asSignedBVLit (ValueExpr (BVValue w v)) = Just (toSigned w v)
|
||||
asSignedBVLit _ = Nothing
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- PreBlock
|
||||
|
||||
@ -912,8 +912,8 @@ bvLit n v = ValueExpr $ mkLit n (toInteger v)
|
||||
(.+) :: 1 <= n => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids (BVType n)
|
||||
x .+ y
|
||||
-- Eliminate add 0
|
||||
| Just 0 <- asBVLit y = x
|
||||
| Just 0 <- asBVLit x = y
|
||||
| Just 0 <- asUnsignedBVLit y = x
|
||||
| Just 0 <- asUnsignedBVLit x = y
|
||||
|
||||
-- Constant folding.
|
||||
| ValueExpr (BVValue w xv) <- x
|
||||
@ -933,11 +933,11 @@ x .+ y
|
||||
| ValueExpr (BVValue _ _) <- x = y .+ x
|
||||
|
||||
-- Reorganize addition by constant to offset.
|
||||
| Just (BVAdd w x_base (asBVLit -> Just x_off)) <- asApp x
|
||||
| Just (BVAdd w x_base (asUnsignedBVLit -> Just x_off)) <- asApp x
|
||||
, ValueExpr (BVValue _ y_off) <- y
|
||||
= x_base .+ bvLit w (x_off + y_off)
|
||||
|
||||
| Just (BVAdd w y_base (asBVLit -> Just y_off)) <- asApp y
|
||||
| Just (BVAdd w y_base (asUnsignedBVLit -> Just y_off)) <- asApp y
|
||||
, ValueExpr (BVValue _ x_off) <- x
|
||||
= y_base .+ bvLit w (x_off + y_off)
|
||||
|
||||
@ -953,12 +953,12 @@ x .- y
|
||||
-- | Performs a multiplication of two bitvector values.
|
||||
(.*) :: (1 <= n) => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids (BVType n)
|
||||
x .* y
|
||||
| Just 0 <- asBVLit x = x
|
||||
| Just 1 <- asBVLit x = y
|
||||
| Just 0 <- asBVLit y = y
|
||||
| Just 1 <- asBVLit y = x
|
||||
| Just 0 <- asUnsignedBVLit x = x
|
||||
| Just 1 <- asUnsignedBVLit x = y
|
||||
| Just 0 <- asUnsignedBVLit y = y
|
||||
| Just 1 <- asUnsignedBVLit y = x
|
||||
|
||||
| Just xv <- asBVLit x, Just yv <- asBVLit y =
|
||||
| Just xv <- asUnsignedBVLit x, Just yv <- asUnsignedBVLit y =
|
||||
bvLit (typeWidth x) (xv * yv)
|
||||
| otherwise = app $ BVMul (typeWidth x) x y
|
||||
|
||||
@ -969,7 +969,7 @@ bvNeg n = bvLit (typeWidth n) 0 .- n
|
||||
-- | Bitwise complement
|
||||
bvComplement :: (1 <= n) => Expr ids (BVType n) -> Expr ids (BVType n)
|
||||
bvComplement x
|
||||
| Just xv <- asBVLit x = bvLit (typeWidth x) (Bits.complement xv)
|
||||
| Just xv <- asUnsignedBVLit x = bvLit (typeWidth x) (Bits.complement xv)
|
||||
-- not (not p) = p
|
||||
| Just (BVComplement _ y) <- asApp x = y
|
||||
| otherwise = app $ BVComplement (typeWidth x) x
|
||||
@ -977,35 +977,35 @@ bvComplement x
|
||||
-- | Bitwise and
|
||||
(.&.) :: (1 <= n) => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids (BVType n)
|
||||
x .&. y
|
||||
| Just xv <- asBVLit x, Just yv <- asBVLit y =
|
||||
| Just xv <- asUnsignedBVLit x, Just yv <- asUnsignedBVLit y =
|
||||
bvLit (typeWidth x) (xv Bits..&. yv)
|
||||
-- Eliminate and when one argument is maxUnsigned
|
||||
| Just xv <- asBVLit x, xv == maxUnsigned (typeWidth x) = y
|
||||
| Just yv <- asBVLit y, yv == maxUnsigned (typeWidth x) = x
|
||||
| Just xv <- asUnsignedBVLit x, xv == maxUnsigned (typeWidth x) = y
|
||||
| Just yv <- asUnsignedBVLit y, yv == maxUnsigned (typeWidth x) = x
|
||||
-- Cancel when and with 0.
|
||||
| Just 0 <- asBVLit x = x
|
||||
| Just 0 <- asBVLit y = y
|
||||
| Just 0 <- asUnsignedBVLit x = x
|
||||
| Just 0 <- asUnsignedBVLit y = y
|
||||
-- Idempotence
|
||||
| x == y = x
|
||||
|
||||
-- Make literal the second argument (simplifies later cases)
|
||||
| isJust (asBVLit x) = assert (isNothing (asBVLit y)) $ y .&. x
|
||||
| isJust (asUnsignedBVLit x) = assert (isNothing (asUnsignedBVLit y)) $ y .&. x
|
||||
|
||||
--(x1 .&. x2) .&. y = x1 .&. (x2 .&. y) -- Only apply when x2 and y is a lit
|
||||
| isJust (asBVLit y)
|
||||
| isJust (asUnsignedBVLit y)
|
||||
, Just (BVAnd _ x1 x2) <- asApp x
|
||||
, isJust (asBVLit x2) =
|
||||
, isJust (asUnsignedBVLit x2) =
|
||||
x1 .&. (x2 .&. y)
|
||||
|
||||
-- (x1 .|. x2) .&. y = (x1 .&. y) .|. (x2 .&. y) -- Only apply when y and x2 is a lit.
|
||||
| isJust (asBVLit y)
|
||||
| isJust (asUnsignedBVLit y)
|
||||
, Just (BVOr _ x1 x2) <- asApp x
|
||||
, isJust (asBVLit x2) =
|
||||
, isJust (asUnsignedBVLit x2) =
|
||||
(x1 .&. y) .|. (x2 .&. y)
|
||||
-- x .&. (y1 .|. y2) = (y1 .&. x) .|. (y2 .&. x) -- Only apply when x and y2 is a lit.
|
||||
| isJust (asBVLit x)
|
||||
| isJust (asUnsignedBVLit x)
|
||||
, Just (BVOr _ y1 y2) <- asApp y
|
||||
, isJust (asBVLit y2) =
|
||||
, isJust (asUnsignedBVLit y2) =
|
||||
(y1 .&. x) .|. (y2 .&. x)
|
||||
|
||||
-- Default case
|
||||
@ -1014,14 +1014,14 @@ x .&. y
|
||||
-- | Bitwise or
|
||||
(.|.) :: (1 <= n) => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids (BVType n)
|
||||
x .|. y
|
||||
| Just xv <- asBVLit x, Just yv <- asBVLit y =
|
||||
| Just xv <- asUnsignedBVLit x, Just yv <- asUnsignedBVLit y =
|
||||
bvLit (typeWidth x) (xv Bits..|. yv)
|
||||
-- Cancel or when one argument is maxUnsigned
|
||||
| Just xv <- asBVLit x, xv == maxUnsigned (typeWidth x) = x
|
||||
| Just yv <- asBVLit y, yv == maxUnsigned (typeWidth x) = y
|
||||
| Just xv <- asUnsignedBVLit x, xv == maxUnsigned (typeWidth x) = x
|
||||
| Just yv <- asUnsignedBVLit y, yv == maxUnsigned (typeWidth x) = y
|
||||
-- Eliminate "or" when one argument is 0
|
||||
| Just 0 <- asBVLit x = y
|
||||
| Just 0 <- asBVLit y = x
|
||||
| Just 0 <- asUnsignedBVLit x = y
|
||||
| Just 0 <- asUnsignedBVLit y = x
|
||||
-- Idempotence
|
||||
| x == y = x
|
||||
-- Default case
|
||||
@ -1031,8 +1031,8 @@ x .|. y
|
||||
bvXor :: (1 <= n) => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids (BVType n)
|
||||
bvXor x y
|
||||
-- Eliminate xor with 0.
|
||||
| Just 0 <- asBVLit x = y
|
||||
| Just 0 <- asBVLit y = x
|
||||
| Just 0 <- asUnsignedBVLit x = y
|
||||
| Just 0 <- asUnsignedBVLit y = x
|
||||
-- Eliminate xor with self.
|
||||
| x == y = bvLit (typeWidth x) (0::Integer)
|
||||
-- If this is a single bit comparison with a constant, resolve to Boolean operation.
|
||||
@ -1054,7 +1054,7 @@ x .=. y
|
||||
| ValueExpr BVValue{} <- x = y .=. x
|
||||
|
||||
-- Rewrite "base + offset = constant" to "base = constant - offset".
|
||||
| Just (BVAdd w x_base (asBVLit -> Just x_off)) <- asApp x
|
||||
| Just (BVAdd w x_base (asUnsignedBVLit -> Just x_off)) <- asApp x
|
||||
, ValueExpr (BVValue _ yv) <- y =
|
||||
app $ Eq x_base (bvLit w (yv - x_off))
|
||||
-- Rewrite "u - v == c" to "u = c + v".
|
||||
@ -1184,8 +1184,8 @@ bvRor v n = bvShr v n .|. bvShl v bits_less_n
|
||||
-- and right shift moves bits to lower-order positions.
|
||||
bvShr :: 1 <= n => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids (BVType n)
|
||||
bvShr x y
|
||||
| Just 0 <- asBVLit y = x
|
||||
| Just 0 <- asBVLit x = x
|
||||
| Just 0 <- asUnsignedBVLit y = x
|
||||
| Just 0 <- asUnsignedBVLit x = x
|
||||
| otherwise = app $ BVShr (typeWidth x) x y
|
||||
|
||||
bvSar :: 1 <= n => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids (BVType n)
|
||||
@ -1193,20 +1193,20 @@ bvSar x y = app $ BVSar (typeWidth x) x y
|
||||
|
||||
bvShl :: 1 <= n => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids (BVType n)
|
||||
bvShl x y
|
||||
| Just 0 <- asBVLit y = x
|
||||
| Just 0 <- asUnsignedBVLit y = x
|
||||
|
||||
| Just xv <- asBVLit x
|
||||
, Just yv <- asBVLit y =
|
||||
| Just xv <- asUnsignedBVLit x
|
||||
, Just yv <- asUnsignedBVLit y =
|
||||
assert (yv <= toInteger (maxBound :: Int)) $
|
||||
bvLit (typeWidth x) (xv `Bits.shiftL` fromInteger yv)
|
||||
|
||||
-- Replace "(x >> c) << c" with (x .&. - 2^c)
|
||||
| Just yv <- asBVLit y
|
||||
, Just (BVShr w x_base (asBVLit -> Just x_shft)) <- asApp x
|
||||
| Just yv <- asUnsignedBVLit y
|
||||
, Just (BVShr w x_base (asUnsignedBVLit -> Just x_shft)) <- asApp x
|
||||
, x_shft == yv =
|
||||
x_base .&. bvLit w (negate (2^x_shft) ::Integer)
|
||||
|
||||
| Just yv <- asBVLit y
|
||||
| Just yv <- asUnsignedBVLit y
|
||||
, yv >= natValue (typeWidth x) = bvLit (typeWidth x) (0 :: Integer)
|
||||
|
||||
| otherwise = app $ BVShl (typeWidth x) x y
|
||||
@ -1216,7 +1216,7 @@ bvShl x y
|
||||
-- 'uext'' docs.
|
||||
bvTrunc' :: (1 <= m, m+1 <= n) => NatRepr m -> Expr ids (BVType n) -> Expr ids (BVType m)
|
||||
bvTrunc' w e0
|
||||
| Just v <- asBVLit e0 =
|
||||
| Just v <- asUnsignedBVLit e0 =
|
||||
bvLit w v
|
||||
| Just Refl <- testEquality (typeWidth e0) w =
|
||||
e0
|
||||
@ -1261,37 +1261,43 @@ bvTrunc w e =
|
||||
Right Refl -> e
|
||||
|
||||
-- | Unsigned less than
|
||||
bvUlt :: Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids BoolType
|
||||
bvUlt :: (1 <= n) => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids BoolType
|
||||
bvUlt x y
|
||||
| Just xv <- asBVLit x, Just yv <- asBVLit y = boolValue (xv < yv)
|
||||
| Just xv <- asUnsignedBVLit x, Just yv <- asUnsignedBVLit y = boolValue (xv < yv)
|
||||
| x == y = false
|
||||
| otherwise =
|
||||
case typeRepr x of
|
||||
BVTypeRepr _ -> app $ BVUnsignedLt x y
|
||||
| otherwise = app $ BVUnsignedLt x y
|
||||
|
||||
-- | Unsigned less than or equal.
|
||||
bvUle :: Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids BoolType
|
||||
bvUle x y = boolNot (bvUlt y x)
|
||||
bvUle :: (1 <= n) => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids BoolType
|
||||
bvUle x y
|
||||
| Just xv <- asUnsignedBVLit x, Just yv <- asUnsignedBVLit y = boolValue (xv <= yv)
|
||||
| x == y = true
|
||||
| otherwise = app $ BVUnsignedLe x y
|
||||
|
||||
-- | Signed less than
|
||||
bvSlt :: (1 <= n) => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids BoolType
|
||||
bvSlt x y
|
||||
| Just xv <- asBVLit x, Just yv <- asBVLit y = boolValue (xv < yv)
|
||||
| Just xv <- asSignedBVLit x, Just yv <- asSignedBVLit y = boolValue (xv < yv)
|
||||
| x == y = false
|
||||
| otherwise =
|
||||
case typeRepr x of
|
||||
BVTypeRepr _ -> app $ BVSignedLt x y
|
||||
| otherwise = app $ BVSignedLt x y
|
||||
|
||||
-- | Signed less than
|
||||
bvSle :: (1 <= n) => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids BoolType
|
||||
bvSle x y
|
||||
| Just xv <- asSignedBVLit x, Just yv <- asSignedBVLit y = boolValue (xv <= yv)
|
||||
| x == y = true
|
||||
| otherwise = app $ BVSignedLe x y
|
||||
|
||||
-- | Returns bit at index given by second argument, 0 being lsb
|
||||
-- If the bit index is greater than or equal to n, then the result is zero.
|
||||
bvBit :: (1 <= n) => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids BoolType
|
||||
bvBit x y
|
||||
| Just xv <- asBVLit x
|
||||
, Just yv <- asBVLit y =
|
||||
| Just xv <- asUnsignedBVLit x
|
||||
, Just yv <- asUnsignedBVLit y =
|
||||
boolValue (xv `Bits.testBit` fromInteger yv)
|
||||
| Just (Trunc xe w) <- asApp x
|
||||
, Just LeqProof <- testLeq n1 (typeWidth xe)
|
||||
, Just yv <- asBVLit y = assert (0 <= yv && yv < natValue w) $
|
||||
, Just yv <- asUnsignedBVLit y = assert (0 <= yv && yv < natValue w) $
|
||||
bvBit xe (ValueExpr (BVValue (typeWidth xe) yv))
|
||||
|
||||
| otherwise =
|
||||
@ -1332,7 +1338,7 @@ sext w e =
|
||||
uext' :: (1 <= m, m+1 <= n, 1 <= n) => NatRepr n -> Expr ids (BVType m) -> Expr ids (BVType n)
|
||||
uext' w e0
|
||||
-- Literal case
|
||||
| Just v <- asBVLit e0 =
|
||||
| Just v <- asUnsignedBVLit e0 =
|
||||
let w0 = typeWidth e0
|
||||
in withLeqProof (leqTrans (leqProof n1 w0) (ltProof w0 w)) $
|
||||
bvLit w v
|
||||
@ -1371,7 +1377,7 @@ least_byte = bvTrunc knownNat
|
||||
-- of the result is different.
|
||||
sadc_overflows :: (1 <= n) => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids BoolType -> Expr ids BoolType
|
||||
sadc_overflows x y c
|
||||
| Just 0 <- asBVLit y, Just False <- asBoolLit c = false
|
||||
| Just 0 <- asUnsignedBVLit y, Just False <- asBoolLit c = false
|
||||
| otherwise = app $ SadcOverflows x y c
|
||||
|
||||
-- | Return true expression is signed add overflows. See
|
||||
@ -1382,7 +1388,7 @@ sadd_overflows x y = sadc_overflows x y false
|
||||
-- | Return true expression if a unsigned add-with carry would overflow.
|
||||
uadc_overflows :: (1 <= n) => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids BoolType -> Expr ids BoolType
|
||||
uadc_overflows x y c
|
||||
| Just 0 <- asBVLit y, Just False <- asBoolLit c = false
|
||||
| Just 0 <- asUnsignedBVLit y, Just False <- asBoolLit c = false
|
||||
| otherwise = app $ UadcOverflows x y c
|
||||
|
||||
-- | Return true expression is unsigned add overflows. See
|
||||
@ -1400,7 +1406,7 @@ usbb_overflows :: (1 <= n)
|
||||
-> Expr ids BoolType
|
||||
-> Expr ids BoolType
|
||||
usbb_overflows x y c
|
||||
| Just 0 <- asBVLit y, Just False <- asBoolLit c = false
|
||||
| Just 0 <- asUnsignedBVLit y, Just False <- asBoolLit c = false
|
||||
-- If the borrow bit is zero, this is equivalent to unsigned x < y.
|
||||
| Just False <- asBoolLit c = bvUlt x y
|
||||
| otherwise = app $ UsbbOverflows x y c
|
||||
@ -1422,9 +1428,9 @@ ssbb_overflows :: (1 <= n)
|
||||
-> Expr ids BoolType
|
||||
-> Expr ids BoolType
|
||||
ssbb_overflows x y c
|
||||
| Just 0 <- asBVLit y, Just False <- asBoolLit c = false
|
||||
| Just 0 <- asUnsignedBVLit y, Just False <- asBoolLit c = 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
|
||||
-- FIXME: not true? | Just 0 <- asUnsignedBVLit c = app $ BVSignedLt x y
|
||||
| otherwise = app $ SsbbOverflows x y c
|
||||
|
||||
-- | Return true expression is signed sub overflows.
|
||||
@ -1527,9 +1533,6 @@ boolXor x y
|
||||
-- Default case.
|
||||
| otherwise = app $ XorApp x y
|
||||
|
||||
bvSle :: (1 <= n) => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids BoolType
|
||||
bvSle x y = app (BVSignedLe x y)
|
||||
|
||||
-- | Construct a literal bit vector. The result is undefined if the
|
||||
-- literal does not fit withint the given number of bits.
|
||||
bvKLit :: (KnownNat n, 1 <= n) => Integer -> Expr ids (BVType n)
|
||||
|
||||
@ -765,8 +765,7 @@ def_sh mnem val_setter cf_setter of_setter = defBinary mnem $ \_ii loc val -> do
|
||||
def_shl :: InstructionDef
|
||||
def_shl = def_sh "shl" bvShl set_cf set_of
|
||||
where set_cf w v i =
|
||||
(i `bvUle` bvLit n8 (natValue w))
|
||||
.&&. bvBit v (bvLit w (natValue w) .- uext w i)
|
||||
(i `bvUle` bvLit n8 (natValue w)) .&&. bvBit v (bvLit w (natValue w) .- uext w i)
|
||||
set_of v _ = msb v
|
||||
|
||||
def_shr :: InstructionDef
|
||||
|
||||
Loading…
Reference in New Issue
Block a user